diff options
| author | Gaëtan Gilbert | 2018-09-15 20:09:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-19 17:02:45 +0100 |
| commit | 8202a6394425bfd8db22966fe0ef83441d7b5d04 (patch) | |
| tree | 41387774232caf0b7eec63bdca8ee315d35f6ad6 /theories/Numbers | |
| parent | 7492a1ae8422b3f996f844ae96376c3f88d82e13 (diff) | |
Put #[universes(template)] on all auto template spots in stdlib
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. |