3 files changed, 5 insertions, 14 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index bf0761d3ae..376410658a 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -1323,7 +1323,6 @@ Proof. by move=> x y r2xy; apply/orP; right. Qed.
 
 (** Variant of simpl_pred specialised to the membership operator. **)
 
-#[universes(template)]
 Variant mem_pred T := Mem of pred T.
 
 (**
@@ -1464,7 +1463,6 @@ Implicit Types (mp : mem_pred T).
    Definition Acoll : collective_pred T := [pred x | ...].
  as the collective_pred_of_simpl is _not_ convertible to pred_of_simpl.  **)
 
-#[universes(template)]
 Structure registered_applicative_pred p := RegisteredApplicativePred {
   applicative_pred_value :> pred T;
   _ : applicative_pred_value = p
@@ -1473,21 +1471,18 @@ Definition ApplicativePred p := RegisteredApplicativePred (erefl p).
 Canonical applicative_pred_applicative sp :=
   ApplicativePred (applicative_pred_of_simpl sp).
 
-#[universes(template)]
 Structure manifest_simpl_pred p := ManifestSimplPred {
   simpl_pred_value :> simpl_pred T;
   _ : simpl_pred_value = SimplPred p
 }.
 Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)).
 
-#[universes(template)]
 Structure manifest_mem_pred p := ManifestMemPred {
   mem_pred_value :> mem_pred T;
   _ : mem_pred_value = Mem [eta p]
 }.
 Canonical expose_mem_pred p := ManifestMemPred (erefl (Mem [eta p])).
 
-#[universes(template)]
 Structure applicative_mem_pred p :=
   ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}.
 Canonical check_applicative_mem_pred p (ap : registered_applicative_pred p) :=
@@ -1538,7 +1533,6 @@ End PredicateSimplification.
 
 (**  Qualifiers and keyed predicates.  **)
 
-#[universes(template)]
 Variant qualifier (q : nat) T := Qualifier of {pred T}.
 
 Coercion has_quality n T (q : qualifier n T) : {pred T} :=
@@ -1573,7 +1567,6 @@ Variable T : Type.
 Variant pred_key (p : {pred T}) := DefaultPredKey.
 
 Variable p : {pred T}.
-#[universes(template)]
 Structure keyed_pred (k : pred_key p) :=
   PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}.
 
@@ -1605,7 +1598,6 @@ Section KeyedQualifier.
 
 Variables (T : Type) (n : nat) (q : qualifier n T).
 
-#[universes(template)]
 Structure keyed_qualifier (k : pred_key q) :=
   PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}.
 Definition KeyedQualifier k := PackKeyedQualifier k (erefl q).
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 71abafc22f..9ebdf71329 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -209,7 +209,6 @@ Register abstract_key as plugins.ssreflect.abstract_key.
 Register abstract as plugins.ssreflect.abstract.
 
 (**  Constants for tactic-views  **)
-#[universes(template)]
 Inductive external_view : Type := tactic_view of Type.
 
 (**
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 5e600362b4..0ce3752a51 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -391,19 +391,19 @@ Notation "@^~ x" := (fun f => f x) : fun_scope.
  Definitions and notation for explicit functions with simplification,
  i.e., which simpl and /= beta expand (this is complementary to nosimpl).  **)
 
+#[universes(template)]
+Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT.
+
 Section SimplFun.
 
 Variables aT rT : Type.
 
-#[universes(template)]
-Variant simpl_fun := SimplFun of aT -> rT.
+Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x.
 
-Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
+End SimplFun.
 
 Coercion fun_of_simpl : simpl_fun >-> Funclass.
 
-End SimplFun.
-
 Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope.
 Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope.
 Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope.