Make kernel parametric on the lowest universe and fix #9294

This could be Prop (for compat with usual Coq), Set (for HoTT),
 or actually an arbitrary "i".

Take lower bound of universes into account in pretyping/engine

Reinstate proper elaboration of SProp <= l constraints:

replacing is_small with equality with lbound is _not_ semantics preserving!

lbound = Set

Elaborate template polymorphic inductives with lower bound Prop

This will make more constraints explicit

Check univ constraints with Prop as lower bound for template inductives

Restrict template polymorphic universes to those not bounded from below

Fixes #9294

fix suggested by Matthieu

Try second fix suggested by Matthieu

Take care of modifying elaboration for record declarations as well.

Rebase and export functions for debug

Remove exported functions used while debugging

Add a new typing flag "check_template" and option "-no-template-checl"

This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).

Update checker to the new typing flags structure

Switch on the new template_check flag to allow old unsafe behavior in
indTyping.

This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.

Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while

Fix `Template Check` option name and test it

Add `Unset Template Check` to Coq89.v

Cooking of inductives and template-check tests

Cleanup test-suite file for template check / universes(template) flags

cookind tests

Move test of `Unset Template Check` to the failure/ dir, but comment it
for now

Template test-suite test explanation

Overlays for PR 9918

Overlay for paramcoq

Add overlay for fiat_parsers (-no-template-check)

Add overlay for fiat_crypto_legacy

Update fiat-crypto legacy overlay

Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.

Remove overlay that should no longer be necessary

The setting in the compat file should handle it

Remove now-merged fiat-crypto-legacy overlay

Update `Print Assumptions` to reflect the typing flag for template checking

Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic

Fix pretty printing to print global universe levels properly

Fix printing of template polymorphic universes

Fix pretty printing for template polymorphism on no universe

Fix interaction of template check and universes(template) flag

Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe

Indtyping fixes for template polymorphic Props

Allow explicit template polymorphism again

Adapt to new indTyping interface

Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).

Fix check of meaningfullness of template polymorphism in the kernel.

It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.

Comment on identity non-template-polymorphism

Remove incorrect universes(template) attributes from ssr

simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).

Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance

Remove incorrect uses of #[universes(template)] from the stdlib

Extraction of micromega changes due to moving an ind decl out of a section

Remove incorrect uses of #[universes(template)] from plugins

Fix test-suite files, removing incorrect #[universes(template)] attributes

Remove incorrect #[universes(template)] attributes in test-suite

Fix test-suite

Remove overlays as they have been merged upstream.

17 files changed, 89 insertions, 98 deletions

diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 78bfe480b3..2762bb6b32 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -19,6 +19,47 @@ Require Export Ring_theory.
 Local Open Scope positive_scope.
 Import RingSyntax.
 
+(** Definition of polynomial expressions *)
+#[universes(template)]
+Inductive PExpr {C} : Type :=
+| PEc : C -> PExpr
+| PEX : positive -> PExpr
+| PEadd : PExpr -> PExpr -> PExpr
+| PEsub : PExpr -> PExpr -> PExpr
+| PEmul : PExpr -> PExpr -> PExpr
+| PEopp : PExpr -> PExpr
+| PEpow : PExpr -> N -> PExpr.
+Arguments PExpr : clear implicits.
+
+ (* Definition of multivariable polynomials with coefficients in C :
+    Type [Pol] represents [X1 ... Xn].
+    The representation is Horner's where a [n] variable polynomial
+    (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients
+    are polynomials with [n-1] variables (C[X2..Xn]).
+    There are several optimisations to make the repr compacter:
+    - [Pc c] is the constant polynomial of value c
+       == c*X1^0*..*Xn^0
+    - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables.
+        variable indices are shifted of j in Q.
+       == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn}
+    - [PX P i Q] is an optimised Horner form of P*X^i + Q
+        with P not the null polynomial
+       == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn}
+
+    In addition:
+    - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden
+      since they can be represented by the simpler form (PX P (i+j) Q)
+    - (Pinj i (Pinj j P)) is (Pinj (i+j) P)
+    - (Pinj i (Pc c)) is (Pc c)
+ *)
+
+#[universes(template)]
+Inductive Pol {C} : Type :=
+| Pc : C -> Pol
+| Pinj : positive -> Pol -> Pol
+| PX : Pol -> positive -> Pol -> Pol.
+Arguments Pol : clear implicits.
+
 Section MakeRingPol.
 
  (* Ring elements *)
@@ -96,33 +137,11 @@ Section MakeRingPol.
     match goal with |- ?t == _ => mul_permut_rec t end).
 
 
- (* Definition of multivariable polynomials with coefficients in C :
-    Type [Pol] represents [X1 ... Xn].
-    The representation is Horner's where a [n] variable polynomial
-    (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients
-    are polynomials with [n-1] variables (C[X2..Xn]).
-    There are several optimisations to make the repr compacter:
-    - [Pc c] is the constant polynomial of value c
-       == c*X1^0*..*Xn^0
-    - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables.
-        variable indices are shifted of j in Q.
-       == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn}
-    - [PX P i Q] is an optimised Horner form of P*X^i + Q
-        with P not the null polynomial
-       == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn}
+ Notation PExpr := (PExpr C).
+ Notation Pol := (Pol C).
 
-    In addition:
-    - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden
-      since they can be represented by the simpler form (PX P (i+j) Q)
-    - (Pinj i (Pinj j P)) is (Pinj (i+j) P)
-    - (Pinj i (Pc c)) is (Pc c)
- *)
-
- #[universes(template)]
- Inductive Pol : Type :=
-  | Pc : C -> Pol
-  | Pinj : positive -> Pol -> Pol
-  | PX : Pol -> positive -> Pol -> Pol.
+ Implicit Types pe : PExpr.
+ Implicit Types P : Pol.
 
  Definition P0 := Pc cO.
  Definition P1 := Pc cI.
@@ -152,7 +171,7 @@ Section MakeRingPol.
   | _ => Pinj j P
   end.
 
- Definition mkPinj_pred j P:=
+ Definition mkPinj_pred j P :=
   match j with
   | xH => P
   | xO j => Pinj (Pos.pred_double j) P
@@ -938,18 +957,6 @@ Qed.
  rewrite <- IHm; auto.
  Qed.
 
- (** Definition of polynomial expressions *)
-
- #[universes(template)]
- Inductive PExpr : Type :=
-  | PEc : C -> PExpr
-  | PEX : positive -> PExpr
-  | PEadd : PExpr -> PExpr -> PExpr
-  | PEsub : PExpr -> PExpr -> PExpr
-  | PEmul : PExpr -> PExpr -> PExpr
-  | PEopp : PExpr -> PExpr
-  | PEpow : PExpr -> N -> PExpr.
-
  (** evaluation of polynomial expressions towards R *)
  Definition mk_X j := mkPinj_pred j mkX.
 
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index a99f21ad47..3c72d3268f 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -68,7 +68,7 @@ Require Import EnvRing.
 Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q :=
   match e with
     | PEc c =>  c
-    | PEX _ j =>  env j
+    | PEX j =>  env j
     | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
     | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
     | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
@@ -80,7 +80,7 @@ Lemma Qeval_expr_simpl : forall env e,
   Qeval_expr env e =
   match e with
     | PEc c =>  c
-    | PEX _ j =>  env j
+    | PEX j =>  env j
     | PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
     | PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
     | PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 75801162a7..cddc140f51 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -289,7 +289,6 @@ 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
@@ -892,7 +891,7 @@ Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C :=
     | Pc c => PEc c
     | Pinj j p => xdenorm  (Pos.add j jmp ) p
     | PX p j q   => PEadd
-      (PEmul (xdenorm jmp p) (PEpow (PEX _  jmp) (Npos j)))
+      (PEmul (xdenorm jmp p) (PEpow (PEX jmp) (Npos j)))
       (xdenorm (Pos.succ jmp) q)
   end.
 
@@ -961,7 +960,7 @@ Variable phi_C_of_S :   forall c,  phiS c =  phi (C_of_S c).
 Fixpoint map_PExpr (e : PExpr S) : PExpr C :=
   match e with
     | PEc c => PEc (C_of_S c)
-    | PEX _ p => PEX _ p
+    | PEX p => PEX p
     | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2)
     | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2)
     | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2)
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 56032befba..d6ccf582ae 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -27,7 +27,6 @@ Section S.
   Context {AA  : Type}. (* type of annotations for atoms *)
   Context {AF  : Type}. (* type of formulae identifiers *)
 
-  #[universes(template)]
    Inductive GFormula  : Type :=
   | TT   : GFormula
   | FF   : GFormula
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 79cb6a3a3e..f93fe021f9 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -27,16 +27,18 @@ Set Implicit Arguments.
  * As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up.
  *)
 
+Inductive t {A} : Type :=
+| Empty : t
+| Elt : A -> t
+| Branch : t  -> A -> t  -> t .
+Arguments t : clear implicits.
+
 Section MakeVarMap.
   
   Variable A : Type.
   Variable default : A.
 
-  #[universes(template)]
-  Inductive t  : Type :=
-  | Empty : t
-  | Elt : A -> t
-  | Branch : t  -> A -> t  -> t .
+  Notation t := (t A).
 
   Fixpoint find (vm : t) (p:positive) {struct vm} : A :=
     match vm with
@@ -49,7 +51,6 @@ Section MakeVarMap.
                       end
     end.
 
-
   Fixpoint singleton (x:positive) (v : A) : t :=
     match x with
     | xH => Elt v
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 3ea7635244..c0d22486b5 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -65,7 +65,7 @@ Qed.
 Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z :=
   match e with
     | PEc c => c
-    | PEX _ x => env x
+    | PEX x => env x
     | PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2
     | PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2
     | PEpow e1 n  => Z.pow (Zeval_expr env e1) (Z.of_N n)
@@ -78,7 +78,7 @@ Definition eval_expr := eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x
 Fixpoint Zeval_const  (e: PExpr Z) : option Z :=
   match e with
   | PEc c => Some c
-  | PEX _ x => None
+  | PEX x => None
   | PEadd e1 e2 => map_option2 (fun x y => Some (x + y))
                                (Zeval_const e1) (Zeval_const e2)
   | PEmul e1 e2 => map_option2 (fun x y => Some (x * y))
@@ -742,7 +742,7 @@ Module Vars.
 Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t :=
   match e with
   | PEc _ => Vars.empty
-  | PEX _ x => Vars.singleton x
+  | PEX x => Vars.singleton x
   | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 =>
     let v1 := vars_of_pexpr e1 in
     let v2 := vars_of_pexpr e2 in
@@ -774,10 +774,10 @@ Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type}
   end.
 
 Definition bound_var (v : positive) : Formula Z :=
-  Build_Formula (PEX _ v) OpGe (PEc 0).
+  Build_Formula (PEX v) OpGe (PEc 0).
 
 Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z :=
-  Build_Formula (PEX _ x) OpEq (PEsub (PEX _ y) (PEX _ t)).
+  Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)).
 
 Section BOUND.
   Context {TX TG ID : Type}.
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index a64a5a84b3..2e97dfea19 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -556,6 +556,15 @@ let zeq_bool x y =
   | Eq -> true
   | _ -> false
 
+type 'c pExpr =
+| PEc of 'c
+| PEX of positive
+| PEadd of 'c pExpr * 'c pExpr
+| PEsub of 'c pExpr * 'c pExpr
+| PEmul of 'c pExpr * 'c pExpr
+| PEopp of 'c pExpr
+| PEpow of 'c pExpr * n
+
 type 'c pol =
 | Pc of 'c
 | Pinj of positive * 'c pol
@@ -868,15 +877,6 @@ let rec psquare cO cI cadd cmul ceqb = function
   let p3 = psquare cO cI cadd cmul ceqb p2 in
   mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2
 
-type 'c pExpr =
-| PEc of 'c
-| PEX of positive
-| PEadd of 'c pExpr * 'c pExpr
-| PEsub of 'c pExpr * 'c pExpr
-| PEmul of 'c pExpr * 'c pExpr
-| PEopp of 'c pExpr
-| PEpow of 'c pExpr * n
-
 (** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **)
 
 let mk_X cO cI j =
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 0ca0d0c12d..6b92445326 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -77,20 +77,24 @@ Lget i (l ++ delta) = Some a.
 induction l;destruct i;simpl;try congruence;auto.
 Qed.
 
-Section Store.
-
-Variable A:Type.
-
-#[universes(template)]
-Inductive Poption : Type:=
+Inductive Poption {A} : Type:=
   PSome : A -> Poption
 | PNone : Poption.
+Arguments Poption : clear implicits.
 
-#[universes(template)]
-Inductive Tree : Type :=
+Inductive Tree {A} : Type :=
    Tempty : Tree
  | Branch0 : Tree -> Tree -> Tree
  | Branch1 : A -> Tree -> Tree -> Tree.
+Arguments Tree : clear implicits.
+
+Section Store.
+
+Variable A:Type.
+
+Notation Poption := (Poption A).
+Notation Tree := (Tree A).
+
 
 Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption :=
   match T with
@@ -179,7 +183,6 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*;
 destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
 Qed.
 
-#[universes(template)]
 Record Store : Type :=
 mkStore  {index:positive;contents:Tree}.
 
@@ -194,7 +197,6 @@ Lemma get_empty : forall i, get i empty = PNone.
 intro i; case i; unfold empty,get; simpl;reflexivity.
 Qed.
 
-#[universes(template)]
 Inductive Full : Store -> Type:=
     F_empty : Full empty
   | F_push : forall a S, Full S -> Full (push a S).
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
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.