Give the same argument name for the record binder of type class

projections and regular records.
Easily fixable backwards incompatibility.

6 files changed, 28 insertions, 15 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 57553f9e1..bf4e6dedd 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -24,6 +24,14 @@ 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/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index b80903dc1..5186014e2 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 (Decidable:=H).
+Definition decide P {H : Decidable P} := Decidable_witness (d:=H).
 
 Ltac _decide_ P H :=
   let b := fresh "b" in
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 3bd9dcd12..ca4bf9cdf 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 Irreflexive} [x] _.
+Arguments irreflexivity {A R i} [x] _.
 
 Hint Resolve irreflexivity : ord.
 
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 17c69d226..4a4451078 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -93,6 +93,13 @@ 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}.
@@ -212,6 +219,7 @@ 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 e8a9940bd..338b5c7f9 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.
-Arguments ZnZ.zdigits [t] Ops.
+Arguments ZnZ.digits [t] Ops : rename.
+Arguments ZnZ.zdigits [t] Ops : rename.
 
 Lemma Pshiftl_nat_Zpower : forall n p,
   Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
diff --git a/toplevel/record.ml b/toplevel/record.ml
index be3fb7c2c..ccb6afbcc 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -263,7 +263,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 	  | Name fid -> try
 	    let kn, term = 
 	      if optci = None && primitive then 
-		  (** Already defined in the kernel silently *)
+		(** Already defined in the kernel silently *)
 		let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
 		  Declare.definition_message fid;
 		  kn, mkProj (Projection.make kn false,mkRel 1)
@@ -388,6 +388,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
     (* else List.map (fun x -> (ExplByPos (1, None), (true, true, true)) :: *)
     (* 		     Impargs.lift_implicits 1 x) fieldimpls *)
   in
+  let record_name = Id.of_string (Unicode.lowercase_first_char (Id.to_string (snd id))) in
   let impl, projs =
     match fields with
     | [(Name proj_name, _, field)] when def ->
@@ -401,9 +402,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 (snd id), inst_type, lift 1 field)) params in
+	  it_mkProd_or_LetIn (mkProd(Name record_name, inst_type, lift 1 field)) params in
 	let proj_body =
-	  it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
+	  it_mkLambda_or_LetIn (mkLambda (Name record_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)
@@ -418,15 +419,14 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
 	in
 	  cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-	let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
 	let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
 	  params arity fieldimpls fields
-	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
+	  ~kind:Method ~name:record_name false (List.map (fun _ -> false) fields) sign
 	in
 	let coers = List.map2 (fun coe pri -> 
 			       Option.map (fun b -> 
 			         if b then Backward, pri else Forward, pri) coe) 
-	  coers priorities 
+	  coers priorities
 	in
 	  IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y))
 			 (List.rev fields) coers (Recordops.lookup_projections ind))
@@ -434,7 +434,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
   let ctx_context =
     List.map (fun (na, b, t) ->
       match Typeclasses.class_of_constr t with
-      | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) (*FIXME: ignore universes?*)
+      | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
       | None -> None)
       params, params
   in
@@ -446,10 +446,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity fieldim
       cl_props = fields;
       cl_projs = projs }
   in
-(*     List.iter3 (fun p sub pri -> *)
-(*       if sub then match p with (_, _, Some p) -> declare_instance_cst true p pri | _ -> ()) *)
-(*       k.cl_projs coers priorities; *)
-  add_class k; impl
+    add_class k; impl
 
 
 let add_constant_class cst =