Cleanup

cryspen · Jun 25, 2024 · bbbd02d · bbbd02d
1 parent 50b195b
commit bbbd02d
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 26 deletions.
diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
@@ -1189,7 +1189,7 @@ impl<'tcx, S: ExprState<'tcx>> SInto<S, Expr> 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<Body: IsBody> {
         Generics<Body>,
         #[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
@@ -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<Self> {
         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
@@ -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 {