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.

23 files changed, 65 insertions, 73 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index bf4e6dedde..57553f9e1a 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -24,14 +24,6 @@ Universe Polymorphism.
   (e.g. induction). Extra "Transparent" might have to be added to
   revert opacity of constants.
 
-Records, Classes.
-
-- The generated binder name of the class argument of projections 
-  in type class declarations is now the same as for the corresponding
-  record name and is the lowercase first character of the class name.
-  E.g for [Class Foo (A : Type) := foo : A -> A], foo's class argument
-  has name [f].
-
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 23861347a8..545325a2a9 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 6b3f6c72f4..d908bcbe21 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 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);
diff --git a/kernel/entries.mli b/kernel/entries.mli
index bf47ff90ee..f6958849b0 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 73a23ef059..39455a7d2a 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 0d5b034049..a231b6cf9d 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 58909ce012..a08184ed5e 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 a3c4d98490..232508bc82 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,
diff --git a/library/declare.ml b/library/declare.ml
index 8ec52d16a5..1c9e10a190 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -382,7 +382,7 @@ let inInductive : inductive_obj -> obj =
 let declare_projections mind =
   let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
     match spec.mind_record with
-    | Some (kns, pjs) -> 
+    | Some (Some (_, kns, pjs)) -> 
       Array.iteri (fun i kn -> 
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
@@ -390,7 +390,7 @@ let declare_projections mind =
 				       IsDefinition StructureComponent) 
 	in
 	  assert(eq_constant kn kn')) kns
-    | None -> ()
+    | Some None | None -> ()
 
 (* for initial declaration *)
 let declare_mind isrecord mie =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index aa0232d19e..ea22396731 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -215,7 +215,7 @@ let oib_equal o1 o2 =
     Array.equal Id.equal o1.mind_consnames o2.mind_consnames
 
 let eq_record x y =
-  Option.equal (fun (x, y) (x', y') -> Array.for_all2 eq_constant x x') x y
+  Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y
 
 let mib_equal m1 m2 =
   Array.equal oib_equal m1.mind_packets m1.mind_packets &&
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 32ac374a1e..f3f58d4371 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1307,7 +1307,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
 let mk_case pb (ci,pred,c,brs) =
   let mib = lookup_mind (fst ci.ci_ind) pb.env in
     match mib.mind_record with
-    | Some (cs, pbs) when Array.length pbs > 0 -> 
+    | Some (Some (_, cs, pbs)) ->
       Reduction.beta_appvect brs.(0) 
 	(Array.map (fun p -> mkProj (Projection.make p false, c)) cs)
     | _ -> mkCase (ci,pred,c,brs)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index fc726c2307..cdb38ecea3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -798,8 +798,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   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 (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 24bf7cbc03..91072dce8c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -334,7 +334,7 @@ let get_constructors env (ind,params) =
 let get_projections env (ind,params) =
   let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
     match mib.mind_record with
-    | Some (projs, pbs) when Array.length projs > 0 -> Some projs
+    | Some (Some (id, projs, pbs)) -> Some projs
     | _ -> None
 
 (* substitution in a signature *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 370f3cee9c..2a6fd6fe7d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -523,8 +523,7 @@ let is_eta_constructor_app env f l1 =
   | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (exp,projs) when Array.length projs > 0
-        && mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
+      | Some (Some (_, exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
         Array.length projs == Array.length l1 - mib.Declarations.mind_nparams
       | _ -> false)
   | _ -> false
@@ -534,7 +533,7 @@ let eta_constructor_app env f l1 term =
   | Construct (((_, i as ind), j), u) ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (projs, _) ->
+      | Some (Some (_, projs, _)) ->
         let npars = mib.Declarations.mind_nparams in
 	let pars, l1' = Array.chop npars l1 in
 	let arg = Array.append pars [|term|] in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 08d7c237d4..e0f6ef25cc 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -205,7 +205,7 @@ let print_polymorphism ref =
        else "not universe polymorphic")
 
 let print_primitive_record mipv = function
-  | Some (ps,_) when Array.length ps > 0 -> 
+  | Some (Some (_, ps,_)) ->
     [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."]
   | _ -> []
     
diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index 5186014e2e..b80903dc12 100644
--- a/theories/Classes/DecidableClass.v
+++ b/theories/Classes/DecidableClass.v
@@ -44,7 +44,7 @@ Qed.
 (** The generic function that should be used to program, together with some
   useful tactics. *)
 
-Definition decide P {H : Decidable P} := Decidable_witness (d:=H).
+Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H).
 
 Ltac _decide_ P H :=
   let b := fresh "b" in
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index ca4bf9cdf2..3bd9dcd12e 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -202,7 +202,7 @@ Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_insta
 Hint Extern 4 (subrelation (flip _) _) => 
   class_apply @subrelation_symmetric : typeclass_instances.
 
-Arguments irreflexivity {A R i} [x] _.
+Arguments irreflexivity {A R Irreflexive} [x] _.
 
 Hint Resolve irreflexivity : ord.
 
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 4a4451078c..17c69d226f 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -93,13 +93,6 @@ Module ZnZ.
     lor         : t -> t -> t;
     land        : t -> t -> t;
     lxor        : t -> t -> t }.
-
- Arguments ZnZ.to_Z t Ops _ : rename.
- Arguments ZnZ.zero t Ops : rename.
- Arguments ZnZ.succ t Ops _ : rename.
- Arguments ZnZ.add_c t Ops _ _ : rename.
- Arguments ZnZ.mul_c t Ops _ _ : rename.
- Arguments ZnZ.compare t Ops _ _ : rename.
  
  Section Specs.
  Context {t : Type}{ops : Ops t}.
@@ -219,7 +212,6 @@ Module ZnZ.
  End Specs.
 
  Arguments Specs {t} ops.
- Arguments ZnZ.spec_0 t ops Specs : rename.
 
  (** Generic construction of double words *)
 
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 338b5c7f94..e8a9940bd0 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -20,8 +20,8 @@ Arguments mk_zn2z_ops [t] ops.
 Arguments mk_zn2z_ops_karatsuba [t] ops.
 Arguments mk_zn2z_specs [t ops] specs.
 Arguments mk_zn2z_specs_karatsuba [t ops] specs.
-Arguments ZnZ.digits [t] Ops : rename.
-Arguments ZnZ.zdigits [t] Ops : rename.
+Arguments ZnZ.digits [t] Ops.
+Arguments ZnZ.zdigits [t] Ops.
 
 Lemma Pshiftl_nat_Zpower : forall n p,
   Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 9de0edea81..1823e3a89a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -104,8 +104,9 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
   let abs_ctx = Univ.instantiate_univ_context abs_ctx in
   let univs = Univ.UContext.union abs_ctx univs in
   let record = match mib.mind_record with
+    | Some (Some (id, _, _)) -> Some (Some id)
+    | Some None -> Some None
     | None -> None
-    | Some (_, a) -> Some (Array.length a > 0)
   in
   { mind_entry_record = record;
     mind_entry_finite = mib.mind_finite;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ccb6afbcc9..dfeedfbc83 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -226,7 +226,7 @@ let instantiate_possibly_recursive_type indu paramdecls fields =
   Termops.substl_rel_context (subst@[mkIndU indu]) fields
 
 (* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
+let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let u = Inductive.inductive_instance mib in
@@ -236,15 +236,15 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
   let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
-  let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
+  let x = Name binder_name in
   let fields = instantiate_possibly_recursive_type indu paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
   let primitive = 
     if !primitive_flag then 
       let is_primitive = 
 	match mib.mind_record with
-	| Some (projs, _) -> Array.length projs > 0
-	| None -> false
+	| Some (Some _) -> true
+	| Some None | None -> false
       in
 	if not is_primitive then 
 	  Flags.if_verbose msg_warning
@@ -345,6 +345,11 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity fieldim
   let args = Termops.extended_rel_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
+  let binder_name = 
+    match name with
+    | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) 
+    | Some n -> n
+  in
   let mie_ind =
     { mind_entry_typename = id;
       mind_entry_arity = arity;
@@ -353,7 +358,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity fieldim
   in
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
-      mind_entry_record = Some !primitive_flag;
+      mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
       mind_entry_finite = finite;
       mind_entry_inds = [mie_ind];
       mind_entry_polymorphic = poly;
@@ -362,7 +367,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity fieldim
   let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
-  let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
+  let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
   let build = ConstructRef cstr in
   let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
   Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
@@ -378,17 +383,14 @@ let implicits_of_context ctx =
     1 (List.rev (Anonymous :: (List.map pi1 ctx)))
 
 let declare_class finite def poly ctx id idbuild paramimpls params arity fieldimpls fields
-    ?(kind=StructureComponent) ?name is_coe coers priorities sign =
+    ?(kind=StructureComponent) is_coe coers priorities sign =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
-    (* if def then *)
-      let len = List.length params in
-      let impls = implicits_of_context params in
-	 List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
-    (* else List.map (fun x -> (ExplByPos (1, None), (true, true, true)) :: *)
-    (* 		     Impargs.lift_implicits 1 x) fieldimpls *)
+    let len = List.length params in
+    let impls = implicits_of_context params in
+      List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
   in
-  let record_name = Id.of_string (Unicode.lowercase_first_char (Id.to_string (snd id))) in
+  let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
   let impl, projs =
     match fields with
     | [(Name proj_name, _, field)] when def ->
@@ -402,9 +404,9 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
 	let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
 	let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in
 	let proj_type =
-	  it_mkProd_or_LetIn (mkProd(Name record_name, inst_type, lift 1 field)) params in
+	  it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
 	let proj_body =
-	  it_mkLambda_or_LetIn (mkLambda (Name record_name, inst_type, mkRel 1)) params in
+	  it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
 	let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in
 	let proj_cst = Declare.declare_constant proj_name
 	  (DefinitionEntry proj_entry, IsDefinition Definition)
@@ -421,7 +423,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
     | _ ->
 	let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
 	  params arity fieldimpls fields
-	  ~kind:Method ~name:record_name false (List.map (fun _ -> false) fields) sign
+	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
 	in
 	let coers = List.map2 (fun coe pri -> 
 			       Option.map (fun b -> 
diff --git a/toplevel/record.mli b/toplevel/record.mli
index befa5f72c0..2422b45bd2 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -21,7 +21,7 @@ val primitive_flag : bool ref
    as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
+  inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
   coercion_flag list -> manual_explicitation list list -> rel_context ->
   (Name.t * bool) list * constant option list