6 files changed, 1 insertions, 9 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index b4300da4d5..3736bc47a5 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -730,7 +730,6 @@ Qed.
 
 (* The input: syntax of a field expression *)
 
-#[universes(template)]
 Inductive FExpr : Type :=
  | FEO : FExpr
  | FEI : FExpr
@@ -763,7 +762,6 @@ Strategy expand [FEeval].
 
 (* The result of the normalisation *)
 
-#[universes(template)]
 Record linear : Type := mk_linear {
    num : PExpr C;
    denum : PExpr C;
@@ -946,7 +944,6 @@ induction e2; intros p1 p2;
   now rewrite <- PEpow_mul_r.
 Qed.
 
-#[universes(template)]
 Record rsplit : Type := mk_rsplit {
    rsplit_left : PExpr C;
    rsplit_common : PExpr C;
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index b024f65988..a98a963207 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -740,7 +740,6 @@ Ltac abstract_ring_morphism set ext rspec :=
   | _ => fail 1 "bad ring structure"
   end.
 
-#[universes(template)]
 Record hypo : Type := mkhypo {
    hypo_type : Type;
    hypo_proof : hypo_type
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index 6a8c514a7b..048c8eecf9 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -32,7 +32,6 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x.
    with coefficients in C :
  *)
 
-#[universes(template)]
  Inductive Pol : Type :=
   | Pc : C -> Pol
   | PX : Pol -> positive -> positive -> Pol -> Pol. 
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 9d56084fd4..092114ff0b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -121,7 +121,6 @@ Section MakeRingPol.
     - (Pinj i (Pc c)) is (Pc c)
  *)
 
- #[universes(template)]
  Inductive Pol : Type :=
   | Pc : C -> Pol
   | Pinj : positive -> Pol -> Pol
@@ -909,7 +908,6 @@ Section MakeRingPol.
 
  (** Definition of polynomial expressions *)
 
- #[universes(template)]
  Inductive PExpr : Type :=
   | PEO : PExpr
   | PEI : PExpr            
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 8f24b281c6..dc45853458 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -540,7 +540,6 @@ Section AddRing.
  Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
  Variable req : R -> R -> Prop. *)
 
-#[universes(template)]
 Inductive ring_kind : Type :=
 | Abstract
 | Computational
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index eb75fca0a1..b456d2eed2 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -151,7 +151,7 @@ let ic_unsafe c = (*FIXME remove *)
 let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
-  let univs = UState.restrict_universe_context univs vars in
+  let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
   let () = Declare.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in