7 files changed, 11 insertions, 3 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
diff --git a/plugins/micromega/itv.ml b/plugins/micromega/itv.ml
index dc1df7ec9f..44cad820ed 100644
--- a/plugins/micromega/itv.ml
+++ b/plugins/micromega/itv.ml
@@ -11,10 +11,11 @@
 (** Intervals (extracted from mfourier.ml) *)
 
 open Num
+
   (** The type of intervals is *)
   type interval = num option * num option
-      (** None models the absence of bound i.e. infinity *)
-      (** As a result,
+      (** None models the absence of bound i.e. infinity
+          As a result,
           - None , None   -> \]-oo,+oo\[
           - None , Some v -> \]-oo,v\]
           - Some v, None  -> \[v,+oo\[
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index f5e9a9f34c..23f3470d77 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -103,7 +103,7 @@ module Poly : sig
 
 end
 
-type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (** Representation of linear constraints *)
+type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (* Representation of linear constraints *)
 and op = Eq | Ge | Gt
 
 val eval_op : op -> Num.num -> Num.num -> bool
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index 8d8c6ea90b..4465aa1ee1 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -20,6 +20,7 @@ type iset = unit IMap.t
 
 type tableau = Vect.t IMap.t (** Mapping basic variables to their equation.
                                  All variables >= than a threshold rst are restricted.*)
+
 module Restricted =
   struct
     type t =