Merge pull request #762 from hacspec/add-use-super-refinement

fix(hax-lib): `use super::*` in refinement expansion
hacspec · Jul 10, 2024 · 45be3ca · 45be3ca
2 parents b462111 + 2dd6c10
commit 45be3ca
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
@@ -820,6 +820,9 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::
     quote! {
         #[allow(non_snake_case)]
         mod #module_ident {
+            #[allow(unused_imports)]
+            use super::*;
+
             #refinement_item
 
             #newtype_as_ref_attr
@@ -828,7 +831,9 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::
 
             #[::hax_lib::exclude]
             impl #generics ::hax_lib::Refinement for #ident <#generics_args> {
+
                 type InnerType = #inner_ty;
+
                 fn new(x: Self::InnerType) -> Self {
                     #debug_assert
                     Self(x)