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

projections and regular records.
Easily fixable backwards incompatibility.

1 files changed, 8 insertions, 0 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 17c69d226f..4a4451078c 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 *)