Update the computation of the implicit parameters

AeneasVerif · Sep 9, 2024 · d7f6555 · d7f6555
1 parent fd3c5a5
commit d7f6555
Show file tree

Hide file tree

Showing 4 changed files with 243 additions and 59 deletions.
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
@@ -1481,7 +1481,7 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl)
     (variant : variant) : string =
   (* Replace the name of the variant if the user annotated it with the [rename] attribute. *)
   let variant =
-    Option.value variant.attr_info.rename ~default:variant.variant_name
+    Option.value variant.variant_attr_info.rename ~default:variant.variant_name
   in
   match backend () with
   | FStar | Coq | HOL4 ->

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
@@ -792,7 +792,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
                   FieldId.mapi
                     (fun fid (field : field) ->
                       ( fid,
-                        ctx_compute_field_name def field.attr_info ctx
+                        ctx_compute_field_name def field.field_attr_info ctx
                           def.item_meta.name fid field.field_name ))
                     fields
                 in