diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/DoubleType.v | 2 |
2 files changed, 3 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 *) diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index fe0476e4de..b6441bb76a 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -22,6 +22,7 @@ Section Carry. Variable A : Type. + #[universes(template)] Inductive carry := | C0 : A -> carry | C1 : A -> carry. @@ -44,6 +45,7 @@ Section Zn2Z. first. *) + #[universes(template)] Inductive zn2z := | W0 : zn2z | WW : znz -> znz -> zn2z. |