diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 449f9fea6..bd25cd66b 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1189,7 +1189,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto for rustc_middle::thir::Expr<'tcx> let contents = kind.sinto(s); use crate::rustc_middle::ty::util::IntTypeExt; let repr_type = tcx - .repr_options_of_def(def.did().as_local().unwrap()) + .repr_options_of_def(def.did().expect_local()) .discr_type() .to_ty(s.base().tcx); if repr_type == ty { @@ -3061,7 +3061,7 @@ pub enum ItemKind { Generics, #[value({ let tcx = s.base().tcx; - tcx.repr_options_of_def(s.owner_id().as_local().unwrap()).sinto(s) + tcx.repr_options_of_def(s.owner_id().expect_local()).sinto(s) })] ReprOptions, ), diff --git a/hax-lib-macros/src/syn_ext.rs b/hax-lib-macros/src/syn_ext.rs index 0620fc31f..f3a85b28a 100644 --- a/hax-lib-macros/src/syn_ext.rs +++ b/hax-lib-macros/src/syn_ext.rs @@ -7,16 +7,6 @@ pub struct ExprClosure1 { pub body: syn::Expr, } -// pub trait PatExt { -// // Make sure to remove type ascriptions -// fn untype(mut pat: syn::Pat) -> syn::Pat { -// if let syn::Pat::Type(sub) = pat { -// pat = *sub.pat.clone(); -// } -// pat -// } -// } - impl Parse for ExprClosure1 { fn parse(ps: ParseStream) -> Result { let closure: syn::ExprClosure = Parse::parse(ps as ParseStream)?; diff --git a/hax-lib-macros/src/utils.rs b/hax-lib-macros/src/utils.rs index f6d7c995b..8a998bf78 100644 --- a/hax-lib-macros/src/utils.rs +++ b/hax-lib-macros/src/utils.rs @@ -1,20 +1,6 @@ use crate::prelude::*; use crate::rewrite_self::*; -// pub trait BlockExt { -// /// Bring in the scope of the block quantifiers helpers (the `forall` and `exists` functions) -// fn make_quantifiers_available(&mut self); -// } - -// impl BlockExt for Block { -// fn make_quantifiers_available(&mut self) { -// self.stmts.insert( -// 0, -// Stmt::Item(Item::Verbatim(HaxQuantifiers.to_token_stream())), -// ); -// } -// } - /// `HaxQuantifiers` expands to the definition of the `forall` and `exists` functions pub struct HaxQuantifiers; impl ToTokens for HaxQuantifiers {