aboutsummaryrefslogtreecommitdiff
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.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 951a4ef2b0..9f718cba65 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -28,6 +28,7 @@ Local Open Scope Z_scope.
Module ZnZ.
+ #[universes(template)]
Class Ops (t:Type) := MkOps {
(* Conversion functions with Z *)