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.

2 files changed, 2 insertions, 10 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 4a4451078..17c69d226 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 338b5c7f9..e8a9940bd 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.