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

projections and regular records.
Easily fixable backwards incompatibility.

4 files changed, 12 insertions, 4 deletions

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.