aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v8
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v4
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.