Merge PR #8488: Warning when using automatic template polymorphism

4 files changed, 6 insertions, 0 deletions

diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 4042959b50..eb84b1203d 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -118,6 +118,7 @@ Section MakeRingPol.
     - (Pinj i (Pc c)) is (Pc c)
  *)
 
+ #[universes(template)]
  Inductive Pol : Type :=
   | Pc : C -> Pol
   | Pinj : positive -> Pol -> Pol
@@ -939,6 +940,7 @@ Qed.
 
  (** Definition of polynomial expressions *)
 
+ #[universes(template)]
  Inductive PExpr : Type :=
   | PEc : C -> PExpr
   | PEX : positive -> PExpr
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index f066ea462f..782fab5e68 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -289,6 +289,7 @@ destruct o' ; rewrite H1 ; now rewrite  (Rplus_0_l sor).
  now apply (Rplus_nonneg_nonneg sor).
 Qed.
 
+#[universes(template)]
 Inductive Psatz : Type :=
 | PsatzIn : nat -> Psatz
 | PsatzSquare : PolC -> Psatz
@@ -685,6 +686,7 @@ end.
 Definition  eval_pexpr : PolEnv -> PExpr C -> R :=
  PEeval rplus rtimes rminus ropp phi pow_phi rpow.
 
+#[universes(template)]
 Record Formula (T:Type) : Type := {
   Flhs : PExpr T;
   Fop : Op2;
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 458844e1b9..587f2f1fa4 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -21,6 +21,7 @@ Require Import Bool.
 Set Implicit Arguments.
 
 
+  #[universes(template)]
   Inductive BFormula (A:Type) : Type :=
   | TT   : BFormula A
   | FF   : BFormula A
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 2d2c0bc77a..c888f9af45 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -30,6 +30,7 @@ Section MakeVarMap.
   Variable A : Type.
   Variable default : A.
 
+  #[universes(template)]
   Inductive t  : Type :=
   | Empty : t
   | Leaf : A -> t