Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name

for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.

1 files changed, 3 insertions, 3 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 5b937207fd..51e435d796 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -237,14 +237,14 @@ let subst_mind_packet sub mbp =
     mind_nb_args = mbp.mind_nb_args;
     mind_reloc_tbl = mbp.mind_reloc_tbl }
 
-let subst_mind_record sub (ps, pb as r) =
+let subst_mind_record sub (id, ps, pb as r) =
   let ps' = Array.smartmap (subst_constant sub) ps in
   let pb' = Array.smartmap (subst_const_proj sub) pb in
     if ps' == ps && pb' == pb then r
-    else (ps', pb')
+    else (id, ps', pb')
 
 let subst_mind_body sub mib =
-  { mind_record = Option.smartmap (subst_mind_record sub) mib.mind_record ;
+  { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ;
     mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);