Recordops: unify struc_typ summary record and libobject entry struc_tuple

This requires updating the parameter count at section end, I felt it
was easier to do with rebuild_function but it could be done in
discharge if needed.

Incidentally fixes #12649.

5 files changed, 47 insertions, 30 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c26da8ccc7..e6e5ad8dd4 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -54,34 +54,29 @@ let structure_table =
 let projection_table =
   Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs"
 
-(* TODO: could be unify struc_typ and struc_tuple ? *)
-
-type struc_tuple =
-    constructor * proj_kind list * Constant.t option list
-
-let register_structure env (id,kl,projs) =
-  let open Declarations in
-  let ind = fst id in
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  let n = mib.mind_nparams in
-  let struc =
-    { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
+let register_structure ({ s_CONST = (ind,_); s_PROJ = projs; } as struc) =
   structure_table := Indmap.add ind struc !structure_table;
   projection_table :=
     List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc))
       projs !projection_table
 
-let subst_structure subst (id, kl, projs as obj) =
+let subst_structure subst struc =
   let projs' =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
    List.Smart.map
      (Option.Smart.map (subst_constant subst))
-    projs
+    struc.s_PROJ
   in
-  let id' = Globnames.subst_constructor subst id in
-  if projs' == projs && id' == id then obj else
-    (id',kl,projs')
+  let id' = Globnames.subst_constructor subst struc.s_CONST in
+  if projs' == struc.s_PROJ && id' == struc.s_CONST
+  then struc
+  else { struc with s_CONST = id'; s_PROJ = projs' }
+
+let rebuild_structure env struc =
+  let mib = Environ.lookup_mind (fst (fst struc.s_CONST)) env in
+  let npars = mib.Declarations.mind_nparams in
+  { struc with s_EXPECTEDPARAM = npars }
 
 let lookup_structure indsp = Indmap.find indsp !structure_table
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 955a4e7aae..3be60d5e62 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -27,13 +27,12 @@ type struc_typ = {
   s_CONST : constructor;
   s_EXPECTEDPARAM : int;
   s_PROJKIND : proj_kind list;
-  s_PROJ : Constant.t option list }
-
-type struc_tuple =
-    constructor * proj_kind list * Constant.t option list
+  s_PROJ : Constant.t option list;
+}
 
-val register_structure : Environ.env -> struc_tuple -> unit
-val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
+val register_structure : struc_typ -> unit
+val subst_structure : Mod_subst.substitution -> struc_typ -> struc_typ
+val rebuild_structure : Environ.env -> struc_typ -> struc_typ
 
 (** [lookup_structure isp] returns the struc_typ associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
diff --git a/test-suite/bugs/closed/bug_12649.v b/test-suite/bugs/closed/bug_12649.v
new file mode 100644
index 0000000000..5547de84ff
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12649.v
@@ -0,0 +1,11 @@
+
+
+Module Type A.
+
+  Record baz : Prop := B { }. (* any sort would do *)
+
+End A.
+
+Print A.
+Module Type UseA (c: A). End UseA.
+Print UseA. (* ANOMALY! Int.Map.get's assert false *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 820bcba0b6..d0036e40f9 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -388,23 +388,26 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
 open Typeclasses
 
 let load_structure i (_, structure) =
-  Recordops.register_structure (Global.env()) structure
+  Recordops.register_structure structure
 
 let cache_structure o =
   load_structure 1 o
 
-let subst_structure (subst, (id, kl, projs as obj)) =
+let subst_structure (subst, obj) =
   Recordops.subst_structure subst obj
 
 let discharge_structure (_, x) = Some x
 
-let inStruc : Recordops.struc_tuple -> obj =
+let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s
+
+let inStruc : Recordops.struc_typ -> obj =
   declare_object {(default_object "STRUCTURE") with
     cache_function = cache_structure;
     load_function = load_structure;
     subst_function = subst_structure;
     classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_structure }
+    discharge_function = discharge_structure;
+    rebuild_function = rebuild_structure; }
 
 let declare_structure_entry o =
   Lib.add_anonymous_leaf (inStruc o)
@@ -497,7 +500,15 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = GlobRef.ConstructRef cstr in
     let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in
-    let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
+    let npars = Inductiveops.inductive_nparams (Global.env()) rsp in
+    let struc = {
+      Recordops.s_CONST = cstr;
+      s_PROJ = List.rev sp_projs;
+      s_PROJKIND = List.rev kinds;
+      s_EXPECTEDPARAM = npars;
+    }
+    in
+    let () = declare_structure_entry struc in
     rsp
   in
   List.mapi map record_data
diff --git a/vernac/record.mli b/vernac/record.mli
index e890f80150..38a622977a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -29,8 +29,6 @@ val declare_projections :
   Constr.rel_context ->
     Recordops.proj_kind list * Constant.t option list
 
-val declare_structure_entry : Recordops.struc_tuple -> unit
-
 val definition_structure
   :  universe_decl_expr option
   -> inductive_kind
@@ -46,3 +44,6 @@ val definition_structure
   -> GlobRef.t list
 
 val declare_existing_class : GlobRef.t -> unit
+
+(** Used by elpi *)
+val declare_structure_entry : Recordops.struc_typ -> unit