3 files changed, 4 insertions, 0 deletions
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index ef2c688759..247827597a 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -29,6 +29,7 @@ Bind Scope positive_scope with positive.
 Arguments xO _%positive.
 Arguments xI _%positive.
 
+Register positive as num.pos.type.
 Register xI as num.pos.xI.
 Register xO as num.pos.xO.
 Register xH as num.pos.xH.
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.