aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/CyclicAxioms.v')
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v8
1 files changed, 0 insertions, 8 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 *)