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.

2 files changed, 17 insertions, 23 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