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.

8 files changed, 30 insertions, 23 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 23861347a..545325a2a 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -871,8 +871,8 @@ let rec get_parameters depth n argstk =
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (projs,pbs) when Array.length projs > 0 
-      && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
+    | Some (Some (_,projs,pbs)) when
+	mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 6b3f6c72f..d908bcbe2 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -97,6 +97,15 @@ type wf_paths = recarg Rtree.t
 v}
 *)
 
+(** Record information:
+    If the record is not primitive, then None
+    Otherwise, we get:
+    - The identifier for the binder name of the record in primitive projections.
+    - The constants associated to each projection.
+    - The checked projection bodies. *)
+
+type record_body = (Id.t * constant array * projection_body array) option
+
 type regular_inductive_arity = {
   mind_user_arity : types;
   mind_sort : sorts;
@@ -153,10 +162,7 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : (constant array * projection_body array) option;  
-    (** Whether the inductive type has been declared as a record, 
-	In the case it is primitive we get its projection names and checked
-	projection bodies, otherwise both arrays are empty. *)
+    mind_record : record_body option; (** The record information *)
 
     mind_finite : Decl_kinds.recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 5b937207f..51e435d79 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);
diff --git a/kernel/entries.mli b/kernel/entries.mli
index bf47ff90e..f6958849b 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -41,9 +41,10 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
-  mind_entry_record : bool option; 
-  (** Some true: primitive record
-      Some false: non-primitive record *)
+  mind_entry_record : (Id.t option) option; 
+  (** Some (Some id): primitive record with id the binder name of the record
+      in projections.
+      Some None: non-primitive record *)
   mind_entry_finite : Decl_kinds.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 73a23ef05..39455a7d2 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -661,7 +661,7 @@ exception UndefinableExpansion
     build an expansion function.
     The term built is expecting to be substituted first by 
     a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params
+let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
     mind_consnrealdecls mind_consnrealargs ctx =
   let mp, dp, l = repr_mind kn in
   let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
@@ -674,7 +674,7 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params
 	ci_pp_info = print_info }
   in
   let len = List.length ctx in
-  let x = Name (Id.of_string (Unicode.lowercase_first_char (Id.to_string n))) in
+  let x = Name x in
   let compat_body ccl i = 
     (* [ccl] is defined in context [params;x:rp] *)
     (* [ccl'] is defined in context [params;x:rp;x:rp] *)
@@ -780,7 +780,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
   let pkt = packets.(0) in	  
   let isrecord = 
     match isrecord with
-    | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
+    | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let u = 
 	if p then 
@@ -792,11 +792,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	(try 
 	   let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
-	     compute_projections indsp pkt.mind_typename nparamargs params
+	     compute_projections indsp pkt.mind_typename rid nparamargs params
 	       pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
-	   in Some (kns, projs)
-	 with UndefinableExpansion -> Some ([||], [||]))
-    | Some _ -> Some ([||], [||])
+	   in Some (Some (rid, kns, projs))
+	 with UndefinableExpansion -> Some None)
+    | Some _ -> Some None
     | None -> None
   in
     (* Build the mutual inductive *)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 0d5b03404..a231b6cf9 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -41,7 +41,7 @@ val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutua
 val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
-val compute_projections : pinductive -> Id.t -> 
+val compute_projections : pinductive -> Id.t -> Id.t ->
   int -> Context.rel_context -> int array -> int array -> 
   Context.rel_context -> 
   (constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 58909ce01..a08184ed5 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -297,7 +297,7 @@ let elim_sorts (_,mip) = mip.mind_kelim
 let is_private (mib,_) = mib.mind_private = Some true
 let is_primitive_record (mib,_) = 
   match mib.mind_record with
-  | Some (projs, _) when Array.length projs > 0 -> true
+  | Some (Some _) -> true
   | _ -> false
 
 let extended_rel_list n hyps =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a3c4d9849..232508bc8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -169,11 +169,11 @@ let infer_declaration env kn dcl =
     let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
     let kn, pb = 
       match mib.mind_record with
-      | Some (kns, pbs) -> 
+      | Some (Some (id, kns, pbs)) -> 
 	if i < Array.length pbs then
 	  kns.(i), pbs.(i)
 	else assert false
-      | None -> assert false
+      | _ -> assert false
     in
     let term, typ = pb.proj_eta in
       Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,