Merge pull request #366 from Nadrieril/update-charon

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-bab27dafb31080ef97d48e5589a33c0e95f2eb05
+f54e30a484a373514df354cfe3fd1ba238bdee6b

src/extract/Extract.ml

@@ -1253,8 +1253,10 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   *)
   let ctx, trait_decl =
     match def.kind with
-    | TraitDeclItem (decl_id, _, true) ->
-        let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
+    | TraitDeclItem (trait_ref, _, true) ->
+        let trait_decl =
+          T.TraitDeclId.Map.find trait_ref.trait_decl_id ctx.trans_trait_decls
+        in
         let ctx, _ = ctx_add_trait_self_clause def.item_meta.span ctx in
         let ctx = { ctx with is_provided_method = true } in
         (ctx, Some trait_decl)

src/extract/ExtractBase.ml

@@ -2131,13 +2131,14 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
   *)
   let item_meta =
     match def.kind with
-    | TraitImplItem (_, trait_decl_id, item_name, _) -> (
+    | TraitImplItem (_, trait_decl_ref, item_name, _) -> (
         if Option.is_some def.item_meta.attr_info.rename then def.item_meta
         else
           (* Lookup the declaration. TODO: the trait item impl info
              should directly give us the id of the method declaration. *)
           match
-            TraitDeclId.Map.find_opt trait_decl_id ctx.trans_trait_decls
+            TraitDeclId.Map.find_opt trait_decl_ref.trait_decl_id
+              ctx.trans_trait_decls
           with
           | None -> def.item_meta
           | Some trait_decl -> (