Merge pull request #365 from Nadrieril/update-hax

AeneasVerif · Sep 17, 2024 · 65c4591 · 65c4591
2 parents 0825fda + f770a4d
commit 65c4591
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 13 deletions.
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs
@@ -166,8 +166,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         &mut self,
         span: rustc_span::Span,
         erase_regions: bool,
-        trait_ref: &hax::TraitRef,
+        trait_ref: &hax::Binder<hax::TraitRef>,
     ) -> Result<Option<TraitDeclRef>, Error> {
+        // TODO: handle binder properly
+        let trait_ref = trait_ref.as_ref().hax_skip_binder();
         let trait_id = self.register_trait_decl_id(span, &trait_ref.def_id);
         let parent_trait_refs = Vec::new();
         let generics = self.translate_substs_and_trait_refs(