comments

Author: gares

vernac/record.ml

@@ -542,6 +542,7 @@ let data_name id rdata =
 module Record_decl = struct
   type t = {
     mie : Entries.mutual_inductive_entry;
+    records : Data.t list;
     primitive_proj : bool;
     impls : DeclareInd.one_inductive_impls list;
     globnames : UState.named_universes_entry;
@@ -550,7 +551,6 @@ module Record_decl = struct
     ubinders : UnivNames.universe_binders;
     projections_kind : Decls.definition_object_kind;
     poly : bool;
-    records : Data.t list;
   }
 end
 

vernac/record.mli

@@ -52,9 +52,12 @@ val definition_structure
       }
   end
 
+  (** A record is an inductive [mie] with extra metadata in [records] *)
   module Record_decl : sig
     type t = {
       mie : Entries.mutual_inductive_entry;
+      records : Data.t list;
+      (* TODO: this part could be factored in mie *)
       primitive_proj : bool;
       impls : DeclareInd.one_inductive_impls list;
       globnames : UState.named_universes_entry;
@@ -63,7 +66,6 @@ val definition_structure
       ubinders : UnivNames.universe_binders;
       projections_kind : Decls.definition_object_kind;
       poly : bool;
-      records : Data.t list;
     }
 end