From 8202a6394425bfd8db22966fe0ef83441d7b5d04 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 15 Sep 2018 20:09:15 +0200
Subject: Put #[universes(template)] on all auto template spots in stdlib

---
 theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 1 +
 theories/Numbers/Cyclic/Abstract/DoubleType.v   | 2 ++
 2 files changed, 3 insertions(+)

(limited to 'theories/Numbers')

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.
-- 
cgit v1.2.3