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

projections and regular records.
Easily fixable backwards incompatibility.

2 files changed, 10 insertions, 2 deletions

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.