Merge PR #9918: Fix #9294: critical bug with template polymorphism

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot

93 files changed, 884 insertions, 415 deletions

diff --git a/checker/values.ml b/checker/values.ml
index ac9bc26344..cc9ac1f834 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -219,7 +219,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 01c2b574a2..d00c8cb11a 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -119,6 +119,16 @@ Universes
   GH issue number: #8341
   risk: unlikely to be activated by chance (requires a plugin)
 
+  component: template polymorphism
+  summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though)
+  impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found
+  impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit)
+  fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau)
+  found by: Gilbert using explicit sharing of universes, exploit found for 8.5-8.9 by Pédrot, other variants generating sharing using sections, or using ltac tricks by Sozeau, exploit in 8.4 by Herbelin and Jason Gross by adding new tricks to Sozeau's variants
+  exploit: test-suite/failure/Template.v
+  GH issue number: #9294
+  risk: moderate risk to be activated by chance
+
 Primitive projections
 
   component: primitive projections, guard condition
diff --git a/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst b/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst
new file mode 100644
index 0000000000..87e89a70f1
--- /dev/null
+++ b/doc/changelog/01-kernel/09918-unsound-template-polymorphism.rst
@@ -0,0 +1,30 @@
+- Fix soundness issue with template polymorphism (`#9294
+  <https://github.com/coq/coq/issues/9294>`_)
+
+  Declarations of template-polymorphic inductive types ignored the
+  provenance of the universes they were abstracting on and did not
+  detect if they should be greater or equal to :math:`\Set` in
+  general. Previous universes and universes introduced by the inductive
+  definition could have constraints that prevented their instantiation
+  with e.g. :math:`\Prop`, resulting in unsound instantiations later. The
+  implemented fix only allows abstraction over universes introduced by
+  the inductive declaration, and properly records all their constraints
+  by making them by default only :math:`>= \Prop`. It is also checked
+  that a template polymorphic inductive actually is polymorphic on at
+  least one universe.
+
+  This prevents inductive declarations in sections to be universe
+  polymorphic over section parameters. For a backward compatible fix,
+  simply hoist the inductive definition out of the section.
+  An alternative is to declare the inductive as universe-polymorphic and
+  cumulative in a universe-polymorphic section: all universes and
+  constraints will be properly gathered in this case.
+  See :ref:`Template-polymorphism` for a detailed exposition of the
+  rules governing template-polymorphic types.
+
+  To help users incrementally fix this issue, a command line option
+  `-no-template-check` and a global flag :flag:`Template Check` are
+  available to selectively disable the new check. Use at your own risk.
+
+  (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau
+  and Maxime Dénès).
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index ef183174d7..1611e9dd52 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -70,7 +70,7 @@ and function types over these sorts.
 Formally, we call :math:`\Sort` the set of sorts which is defined by:
 
 .. math::
-   
+
    \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\}
 
 Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and
@@ -436,7 +436,7 @@ instance the identity function over a given type :math:`T` can be written
 this a *reduction* (or a *conversion*) rule we call :math:`β`:
 
 .. math::
-   
+
         E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u}
 
 We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of
@@ -474,14 +474,14 @@ with its value, that is to expand (or unfold) it into its value. This
 reduction is called δ-reduction and shows as follows.
 
 .. inference:: Delta-Local
-   
+
    \WFE{\Gamma}
    (x:=t:T) ∈ Γ
    --------------
    E[Γ] ⊢ x~\triangleright_Δ~t
 
 .. inference:: Delta-Global
-   
+
    \WFE{\Gamma}
    (c:=t:T) ∈ E
    --------------
@@ -499,7 +499,7 @@ destroyed, this reduction differs from δ-reduction. It is called
 ζ-reduction and shows as follows.
 
 .. inference:: Zeta
-   
+
    \WFE{\Gamma}
    \WTEG{u}{U}
    \WTE{\Gamma::(x:=u:U)}{t}{T}
@@ -533,17 +533,17 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`.
 
    .. math::
       f ~:~ ∀ x:\Type(2),~\Type(1)
-   
+
    then
 
    .. math::
       λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1)
-   
+
    We could not allow
 
    .. math::
       λ x:\Type(1).~(f~x) ~\triangleright_η~ f
-   
+
    because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be
    convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`.
 
@@ -665,7 +665,7 @@ a *subtyping* relation inductively defined by:
    .. math::
       [c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' ,~t'~v_{1,1}' … v_{1,m}' ;~…;~
        c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,~t'~v_{k,1}' … v_{k,m}' ]
-   
+
    respectively then
 
    .. math::
@@ -695,7 +695,7 @@ a *subtyping* relation inductively defined by:
 The conversion rule up to subtyping is now exactly:
 
 .. inference:: Conv
-   
+
    E[Γ] ⊢ U : s
    E[Γ] ⊢ t : T
    E[Γ] ⊢ T ≤_{βδιζη} U
@@ -716,13 +716,13 @@ that :math:`t_0` is :math:`λ x:T.~u_0` then one step of β-head reduction of :m
 .. math::
    λ x_1 :T_1 .~… λ x_k :T_k .~(λ x:T.~u_0~t_1 … t_n ) ~\triangleright~
    λ (x_1 :T_1 )…(x_k :T_k ).~(\subst{u_0}{x}{t_1}~t_2 … t_n )
-   
+
 Iterating the process of head reduction until the head of the reduced
 term is no more an abstraction leads to the *β-head normal form* of :math:`t`:
 
 .. math::
    t \triangleright … \triangleright λ x_1 :T_1 .~…λ x_k :T_k .~(v~u_1 … u_m )
-   
+
 where :math:`v` is not an abstraction (nor an application). Note that the head
 normal form must not be confused with the normal form since some :math:`u_i`
 can be reducible. Similar notions of head-normal forms involving δ, ι
@@ -828,7 +828,7 @@ We have to give the type of constants in a global environment :math:`E` which
 contains an inductive definition.
 
 .. inference:: Ind
-	       
+
    \WFE{Γ}
    \ind{p}{Γ_I}{Γ_C} ∈ E
    (a:A)∈Γ_I
@@ -836,7 +836,7 @@ contains an inductive definition.
    E[Γ] ⊢ a : A
 
 .. inference:: Constr
-	       
+
    \WFE{Γ}
    \ind{p}{Γ_I}{Γ_C} ∈ E
    (c:C)∈Γ_C
@@ -917,7 +917,7 @@ condition* for a constant :math:`X` in the following cases:
 + :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i`
 + :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V`
   satisfies the positivity condition for :math:`X`.
-  
+
 Strict positivity
 +++++++++++++++++
 
@@ -931,10 +931,10 @@ cases:
   strictly positively in type :math:`V`
 + :math:`T` converts to :math:`(I~a_1 … a_m~t_1 … t_p )` where :math:`I` is the name of an
   inductive definition of the form
-  
+
   .. math::
      \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_1 ;~…;~c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_n}
-     
+
   (in particular, it is
   not mutually defined and it has :math:`m` parameters) and :math:`X` does not occur in
   any of the :math:`t_i`, and the (instantiated) types of constructor
@@ -998,7 +998,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]`
    (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n}
    ------------------------------------------
    \WF{E;~\ind{p}{Γ_I}{Γ_C}}{}
-   
+
 
 provided that the following side conditions hold:
 
@@ -1052,30 +1052,10 @@ between universes for inductive types in the Type hierarchy.
 Template polymorphism
 +++++++++++++++++++++
 
-Inductive types can be made polymorphic over their arguments
-in :math:`\Type`.
-
-.. flag:: Auto Template Polymorphism
-
-   This option, enabled by default, makes every inductive type declared
-   at level :math:`\Type` (without annotations or hiding it behind a
-   definition) template polymorphic.
-
-   This can be prevented using the ``notemplate`` attribute.
-
-   An inductive type can be forced to be template polymorphic using the
-   ``template`` attribute.
-
-   Template polymorphism and universe polymorphism (see Chapter
-   :ref:`polymorphicuniverses`) are incompatible, so if the later is
-   enabled it will prevail over automatic template polymorphism and
-   cause an error when using the ``template`` attribute.
-
-.. warn:: Automatically declaring @ident as template polymorphic.
-
-   Warning ``auto-template`` can be used to find which types are
-   implicitly declared template polymorphic by :flag:`Auto Template
-   Polymorphism`.
+Inductive types can be made polymorphic over the universes introduced by
+their parameters in :math:`\Type`, if the minimal inferred sort of the
+inductive declarations either mention some of those parameter universes
+or is computed to be :math:`\Prop` or :math:`\Set`.
 
 If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
 for the arity obtained from :math:`A` by replacing its sort with :math:`s`.
@@ -1117,10 +1097,11 @@ provided that the following side conditions hold:
     + there are sorts :math:`s_i`, for :math:`1 ≤ i ≤ k` such that, for
       :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;~…;~I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]`
       we have :math:`(E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}` ;
-    + the sorts :math:`s_i` are such that all eliminations, to
-      :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, are allowed
-      (see Section :ref:`Destructors`).
-
+    + the sorts :math:`s_i` are all introduced by the inductive
+      declaration and have no universe constraints beside being greater
+      than or equal to :math:`\Prop`, and such that all
+      eliminations, to :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`,
+      are allowed (see Section :ref:`Destructors`).
 
 
 Notice that if :math:`I_j~q_1 … q_r` is typable using the rules **Ind-Const** and
@@ -1141,6 +1122,61 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
 :math:`C_i~q_1 … q_r` is mapped to the names chosen in the specific instance of
 :math:`\ind{p}{Γ_I}{Γ_C}`.
 
+.. warning::
+
+   The restriction that sorts are introduced by the inductive
+   declaration prevents inductive types declared in sections to be
+   template-polymorphic on universes introduced previously in the
+   section: they cannot parameterize over the universes introduced with
+   section variables that become parameters at section closing time, as
+   these may be shared with other definitions from the same section
+   which can impose constraints on them.
+
+.. flag:: Auto Template Polymorphism
+
+   This option, enabled by default, makes every inductive type declared
+   at level :math:`\Type` (without annotations or hiding it behind a
+   definition) template polymorphic if possible.
+
+   This can be prevented using the ``notemplate`` attribute.
+
+.. warn:: Automatically declaring @ident as template polymorphic.
+
+   Warning ``auto-template`` can be used to find which types are
+   implicitly declared template polymorphic by :flag:`Auto Template
+   Polymorphism`.
+
+   An inductive type can be forced to be template polymorphic using the
+   ``template`` attribute: it should then fullfill the criterion to
+   be template polymorphic or an error is raised.
+
+.. exn:: Inductive @ident cannot be made template polymorphic.
+
+   This error is raised when the `#[universes(template)]` attribute is
+   on but the inductive cannot be made polymorphic on any universe or be
+   inferred to live in :math:`\Prop` or :math:`\Set`.
+
+   Template polymorphism and universe polymorphism (see Chapter
+   :ref:`polymorphicuniverses`) are incompatible, so if the later is
+   enabled it will prevail over automatic template polymorphism and
+   cause an error when using the ``template`` attribute.
+
+.. flag:: Template Check
+
+   Unsetting option :flag:`Template Check` disables the check of
+   locality of the sorts when abstracting the inductive over its
+   parameters. This is a deprecated and *unsafe* flag that can introduce
+   inconsistencies, it is only meant to help users incrementally update
+   code from Coq versions < 8.10 which did not implement this check.
+   The `Coq89.v` compatibility file sets this flag globally. A global
+   ``-no-template-check`` command line option is also available. Use at
+   your own risk. Use of this flag is recorded in the typing flags
+   associated to a definition but is *not* supported by the |Coq|
+   checker (`coqchk`). It will appear in :g:`Print Assumptions` and
+   :g:`About @ident` output involving inductive declarations that were
+   (potentially unsoundly) assumed to be template polymorphic.
+
+
 In practice, the rule **Ind-Family** is used by |Coq| only when all the
 inductive types of the inductive definition are declared with an arity
 whose sort is in the Type hierarchy. Then, the polymorphism is over
@@ -1154,10 +1190,10 @@ inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicativ
 Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_),
 and otherwise in the Type hierarchy.
 
-Note that the side-condition about allowed elimination sorts in the
-rule **Ind-Family** is just to avoid to recompute the allowed elimination
-sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As
-an example, let us consider the following definition:
+Note that the side-condition about allowed elimination sorts in the rule
+**Ind-Family** avoids to recompute the allowed elimination sorts at each
+instance of a pattern matching (see Section :ref:`Destructors`). As an
+example, let us consider the following definition:
 
 .. example::
 
@@ -1320,7 +1356,7 @@ using the syntax:
    \Match~m~\as~x~\In~I~\_~a~\return~P~\with~
    (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | …
    | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend
-   
+
 The :math:`\as` part can be omitted if either the result type does not depend
 on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m`
 can occur in :math:`P` where it is considered a bound variable). The :math:`\In` part
@@ -1360,7 +1396,7 @@ There is no restriction on the sort of the predicate to be eliminated.
    -----------------------
    [I:∀ x:A,~A′|∀ x:A,~B′]
 
-   
+
 .. inference:: Set & Type
 
    s_1 ∈ \{\Set,\Type(j)\}
@@ -1376,7 +1412,7 @@ is also of sort :math:`\Prop` or is of the morally smaller sort
 :math:`\SProp`.
 
 .. inference:: Prop
-	       
+
    s ∈ \{\SProp,\Prop\}
    --------------------
    [I:\Prop|I→s]
@@ -1404,7 +1440,7 @@ the proof of :g:`or A B` is not accepted:
 
       Fail Definition choice (A B: Prop) (x:or A B) :=
       match x with or_introl _ _ a => true | or_intror _ _ b => false end.
-   
+
 From the computational point of view, the structure of the proof of
 :g:`(or A B)` in this term is needed for computing the boolean value.
 
@@ -1441,7 +1477,7 @@ this type.
 :math:`\Prop` for which more eliminations are allowed.
 
 .. inference:: Prop-extended
-	       
+
    I~\kw{is an empty or singleton definition}
    s ∈ \Sort
    -------------------------------------
@@ -1589,7 +1625,7 @@ An ι-redex is a term of the following form:
 
 .. math::
    \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l )
-   
+
 with :math:`c_{p_i}` the :math:`i`-th constructor of the inductive type :math:`I` with :math:`r`
 parameters.
 
@@ -1636,7 +1672,7 @@ Typing rule
 The typing rule is the expected one for a fixpoint.
 
 .. inference:: Fix
-	       
+
    (E[Γ] ⊢ A_i : s_i )_{i=1… n}
    (E[Γ;~f_1 :A_1 ;~…;~f_n :A_n ] ⊢ t_i : A_i )_{i=1… n}
    -------------------------------------------------------
@@ -1749,7 +1785,7 @@ The reduction for fixpoints is:
 
 .. math::
    (\Fix~f_i \{F\}~a_1 …a_{k_i}) ~\triangleright_ι~ \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i}
-   
+
 when :math:`a_{k_i}` starts with a constructor. This last restriction is needed
 in order to keep strong normalization and corresponds to the reduction
 for primitive recursive operators. The following reductions are now
@@ -1808,11 +1844,11 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution
         {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}
         {\subst{Γ}{c′}{(c′~c)}}}
 
-   
+
 .. math::
    \frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}}
         {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}}
-	
+
 .. math::
    \frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}}
         {\WFTWOLINES{E;~c:U;~E′;~\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}};~
@@ -1853,7 +1889,7 @@ One can consequently derive the following property.
 .. _First-pruning-property:
 
 .. inference:: First pruning property:
-	       
+
    \WF{E;~c:U;~E′}{Γ}
    c~\kw{does not occur in}~E′~\kw{and}~Γ
    --------------------------------------
@@ -1933,5 +1969,3 @@ impredicative system for sort :math:`\Set` become:
    s ∈ \{\Type(i)\}
    ----------------
    [I:\Set|I→ s]
-
-
diff --git a/engine/evd.ml b/engine/evd.ml
index b621a3fe2f..6a721a1a8a 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -702,7 +702,7 @@ let empty = {
 }
 
 let from_env e = 
-  { empty with universes = UState.make (Environ.universes e) }
+  { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) }
 
 let from_ctx ctx = { empty with universes = ctx }
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 5ed016e0d0..cb40e6eadd 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -34,6 +34,7 @@ type t =
    (** The subset of unification variables that can be instantiated with
         algebraic universes as they appear in inferred types only. *)
    uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+   uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *)
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
    uctx_weak_constraints : UPairSet.t
  }
@@ -47,6 +48,7 @@ let empty =
     uctx_univ_variables = LMap.empty;
     uctx_univ_algebraic = LSet.empty;
     uctx_universes = initial_sprop_cumulative;
+    uctx_universes_lbound = Univ.Level.set;
     uctx_initial_universes = initial_sprop_cumulative;
     uctx_weak_constraints = UPairSet.empty; }
 
@@ -54,10 +56,12 @@ let elaboration_sprop_cumul =
   Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
     ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
 
-let make u =
+let make ~lbound u =
   let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
-    { empty with 
-      uctx_universes = u; uctx_initial_universes = u}
+    { empty with
+      uctx_universes = u;
+      uctx_universes_lbound = lbound;
+      uctx_initial_universes = u}
 
 let is_empty ctx =
   ContextSet.is_empty ctx.uctx_local &&
@@ -83,7 +87,7 @@ let union ctx ctx' =
     let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in
     let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in
     let declarenew g =
-      LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
+      LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g
     in
     let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
@@ -99,6 +103,7 @@ let union ctx ctx' =
            else
              let cstrsr = ContextSet.constraints ctx'.uctx_local in
              UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes));
+        uctx_universes_lbound = ctx.uctx_universes_lbound;
         uctx_weak_constraints = weak}
 
 let context_set ctx = ctx.uctx_local
@@ -431,18 +436,19 @@ let check_univ_decl ~poly uctx decl =
       (ContextSet.constraints uctx.uctx_local);
   ctx
 
-let restrict_universe_context (univs, csts) keep =
+let restrict_universe_context ~lbound (univs, csts) keep =
   let removed = LSet.diff univs keep in
   if LSet.is_empty removed then univs, csts
   else
   let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
   let g = UGraph.initial_universes in
-  let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in
+  let g = LSet.fold (fun v g -> if Level.is_small v then g else
+                        UGraph.add_universe v ~lbound ~strict:false g) allunivs g in
   let g = UGraph.merge_constraints csts g in
   let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in
   let csts = UGraph.constraints_for ~kept:allkept g in
   let csts = Constraint.filter (fun (l,d,r) ->
-      not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
+      not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
   (LSet.inter univs keep, csts)
 
 let restrict ctx vars =
@@ -450,7 +456,7 @@ let restrict ctx vars =
   let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars)
       (fst ctx.uctx_names) vars
   in
-  let uctx' = restrict_universe_context ctx.uctx_local vars in
+  let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
 let demote_seff_univs universes uctx =
@@ -497,7 +503,7 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
     else ContextSet.append ctx' uctx.uctx_local in
   let declare g =
     LSet.fold (fun u g ->
-               try UGraph.add_universe u false g
+               try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g
                with UGraph.AlreadyDeclared when sideff -> g)
               levels g
   in
@@ -544,16 +550,17 @@ let new_univ_variable ?loc rigid name
     | None -> add_uctx_loc u loc uctx.uctx_names
   in
   let initial =
-    UGraph.add_universe u false uctx.uctx_initial_universes
+    UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes
   in                                                 
   let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-                uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
+                uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false
+                    u uctx.uctx_universes;
                 uctx_initial_universes = initial}
   in uctx', u
 
-let make_with_initial_binders e us =
-  let uctx = make e in
+let make_with_initial_binders ~lbound e us =
+  let uctx = make ~lbound e in
   List.fold_left
     (fun uctx { CAst.loc; v = id } ->
        fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
@@ -561,10 +568,10 @@ let make_with_initial_binders e us =
 
 let add_global_univ uctx u =
   let initial =
-    UGraph.add_universe u true uctx.uctx_initial_universes
+    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
   in
   let univs = 
-    UGraph.add_universe u true uctx.uctx_universes
+    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
   in
   { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
                                      uctx_initial_universes = initial;
@@ -679,8 +686,9 @@ let refresh_undefined_univ_variables uctx =
       uctx.uctx_univ_variables LMap.empty
   in
   let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in
-  let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g)
-                                   (ContextSet.levels ctx') g in
+  let lbound = uctx.uctx_universes_lbound in
+  let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g)
+      (ContextSet.levels ctx') g in
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare UGraph.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
@@ -688,14 +696,16 @@ let refresh_undefined_univ_variables uctx =
                uctx_seff_univs = uctx.uctx_seff_univs;
                uctx_univ_variables = vars; uctx_univ_algebraic = alg;
                uctx_universes = univs;
+               uctx_universes_lbound = lbound;
                uctx_initial_universes = initial;
                uctx_weak_constraints = weak; } in
     uctx', subst
 
 let minimize uctx =
   let open UnivMinim in
+  let lbound = uctx.uctx_universes_lbound in
   let ((vars',algs'), us') =
-    normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
+    normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
       uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
   in
   if ContextSet.equal us' uctx.uctx_local then uctx
@@ -709,6 +719,7 @@ let minimize uctx =
         uctx_univ_variables = vars'; 
         uctx_univ_algebraic = algs';
         uctx_universes = universes;
+        uctx_universes_lbound = lbound;
         uctx_initial_universes = uctx.uctx_initial_universes;
         uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) }
 
diff --git a/engine/uState.mli b/engine/uState.mli
index 9689f2e961..52e48c4eeb 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
 
 val empty : t
 
-val make : UGraph.t -> t
+val make : lbound:Univ.Level.t -> UGraph.t -> t
 
-val make_with_initial_binders : UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -88,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
 
 (** {5 Unification} *)
 
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to
    the universes in [keep]. The constraints [csts] are adjusted so
    that transitive constraints between remaining universes (those in
    [keep] and those not in [univs]) are preserved. *)
-val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 1b7c33b9c1..30fdd28997 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -269,11 +269,11 @@ module UPairs = OrderedType.UnorderedPair(Univ.Level)
 module UPairSet = Set.Make (UPairs)
 
 (* TODO check is_small/sprop *)
-let normalize_context_set g ctx us algs weak =
+let normalize_context_set ~lbound g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
+    Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts
   in
   let smallles = if get_set_minimization ()
     then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
@@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak =
   let csts, partition =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-    let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
+    let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g)
                            ctx UGraph.initial_universes
     in
     let add_soft u g =
       if not (Level.is_small u || LSet.mem u ctx)
-      then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+      then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g
       else g
     in
     let g = Constraint.fold
@@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak =
   (* We ignore the trivial Prop/Set <= i constraints. *)
   let noneqs =
     Constraint.filter
-      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+      (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) ||
                            (Level.is_prop l && d == Lt && Level.is_set r)))
       csts
   in
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
index 21f6efe86a..72b432e62f 100644
--- a/engine/univMinim.mli
+++ b/engine/univMinim.mli
@@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-val normalize_context_set : UGraph.t -> ContextSet.t ->
+val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t ->
   universe_opt_subst (* The defined and undefined variables *) ->
   LSet.t (* univ variables that can be substituted by algebraics *) ->
   UPairSet.t (* weak equality constraints *) ->
diff --git a/engine/univops.mli b/engine/univops.mli
index 6cc7868a38..1f1edbed16 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,5 +15,5 @@ open Univ
 val universes_of_constr : constr -> LSet.t
 [@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
-val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
 [@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3f216b0d63..b4798127f9 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -625,7 +625,8 @@ let interp_univ_constraints env evd cstrs =
 let interp_univ_decl env decl =
   let open UState in
   let pl : lident list = decl.univdecl_instance in
-  let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
+  let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env)
+                            (Environ.universes env) pl) in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
   let decl = { univdecl_instance = pl;
     univdecl_extensible_instance = decl.univdecl_extensible_instance;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8d32684b09..44676c9da5 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,6 +87,11 @@ type typing_flags = {
 
   indices_matter: bool;
   (** The universe of an inductive type must be above that of its indices. *)
+
+  check_template : bool;
+  (* If [false] then we don't check that the universes template-polymorphic
+     inductive parameterize on are necessarily local and unbounded from below.
+     This potentially introduces inconsistencies. *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 391b139496..7225671a1e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,6 +26,7 @@ let safe_flags oracle = {
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;
+  check_template = true;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 655094e88b..4a2aeea22d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -59,8 +59,9 @@ type globals = {
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement;
   env_sprop_allowed : bool;
+  env_universes_lbound : Univ.Level.t;
+  env_engagement : engagement
 }
 
 type val_kind =
@@ -119,9 +120,9 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = UGraph.initial_universes;
-    env_engagement = PredicativeSet;
     env_sprop_allowed = false;
-  };
+    env_universes_lbound = Univ.Level.set;
+    env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
   indirect_pterms = Opaqueproof.empty_opaquetab;
@@ -262,8 +263,15 @@ let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
 let indices_matter env = env.env_typing_flags.indices_matter
+let check_template env = env.env_typing_flags.check_template
 
 let universes env = env.env_stratification.env_universes
+let universes_lbound env = env.env_stratification.env_universes_lbound
+
+let set_universes_lbound env lbound =
+  let env_stratification = { env.env_stratification with env_universes_lbound = lbound } in
+  { env with env_stratification }
+
 let named_context env = env.env_named_context.env_named_ctx
 let named_context_val env = env.env_named_context
 let rel_context env = env.env_rel_context.env_rel_ctx
@@ -382,29 +390,30 @@ let check_constraints c env =
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
-let add_universes strict ctx g =
+let add_universes ~lbound ~strict ctx g =
   let g = Array.fold_left
-            (fun g v -> UGraph.add_universe v strict g)
+            (fun g v -> UGraph.add_universe ~lbound ~strict v g)
 	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
     UGraph.merge_constraints (Univ.UContext.constraints ctx) g
 			   
 let push_context ?(strict=false) ctx env =
-  map_universes (add_universes strict ctx) env
+  map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env
 
-let add_universes_set strict ctx g =
+let add_universes_set ~lbound ~strict ctx g =
   let g = Univ.LSet.fold
             (* Be lenient, module typing reintroduces universes and constraints due to includes *)
-	    (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g)
+            (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g)
 	    (Univ.ContextSet.levels ctx) g
   in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
 
 let push_context_set ?(strict=false) ctx env =
-  map_universes (add_universes_set strict ctx) env
+  map_universes (add_universes_set ~lbound:(universes_lbound env) ~strict ctx) env
 
 let push_subgraph (levels,csts) env =
+  let lbound = universes_lbound env in
   let add_subgraph g =
-    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) levels g in
     let newg = UGraph.merge_constraints csts newg in
     (if not (Univ.Constraint.is_empty csts) then
        let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
@@ -428,6 +437,7 @@ let same_flags {
      share_reduction;
      enable_VM;
      enable_native_compiler;
+     check_template;
   } alt =
   check_guarded == alt.check_guarded &&
   check_positive == alt.check_positive &&
@@ -436,7 +446,8 @@ let same_flags {
   indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
-  enable_native_compiler == alt.enable_native_compiler
+  enable_native_compiler == alt.enable_native_compiler &&
+  check_template == alt.check_template
 [@warning "+9"]
 
 let set_typing_flags c env = (* Unsafe *)
@@ -568,11 +579,20 @@ let polymorphic_pind (ind,u) env =
 let type_in_type_ind (mind,_i) env =
   not (lookup_mind mind env).mind_typing_flags.check_universes
 
+let template_checked_ind (mind,_i) env =
+  (lookup_mind mind env).mind_typing_flags.check_template
+
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with 
   | TemplateArity _ -> true
   | RegularArity _ -> false
 
+let template_polymorphic_variables (mind,i) env =
+  match (lookup_mind mind env).mind_packets.(i).mind_arity with
+  | TemplateArity { Declarations.template_param_levels = l; _ } ->
+    List.map_filter (fun level -> level) l
+  | RegularArity _ -> []
+
 let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
   else template_polymorphic_ind ind env
@@ -762,6 +782,22 @@ let is_template_polymorphic env r =
   | IndRef ind -> template_polymorphic_ind ind env
   | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env
 
+let get_template_polymorphic_variables env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> []
+  | ConstRef _c -> []
+  | IndRef ind -> template_polymorphic_variables ind env
+  | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
+
+let is_template_checked env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> false
+  | ConstRef _c -> false
+  | IndRef ind -> template_checked_ind ind env
+  | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
+
 let is_type_in_type env r =
   let open Names.GlobRef in
   match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index e6d814ac7d..f7de98dcfb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -51,8 +51,9 @@ type globals
 
 type stratification = {
   env_universes : UGraph.t;
-  env_engagement : engagement;
   env_sprop_allowed : bool;
+  env_universes_lbound : Univ.Level.t;
+  env_engagement : engagement
 }
 
 type named_context_val = private {
@@ -85,6 +86,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
+val universes_lbound : env -> Univ.Level.t
+val set_universes_lbound : env -> Univ.Level.t -> env
 val rel_context   : env -> Constr.rel_context
 val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
@@ -99,6 +102,7 @@ val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
 val deactivated_guard : env -> bool
 val indices_matter : env -> bool
+val check_template : env -> bool
 
 val is_impredicative_sort : env -> Sorts.t -> bool
 val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -254,7 +258,9 @@ val type_in_type_ind : inductive -> env -> bool
 
 (** Old-style polymorphism *)
 val template_polymorphic_ind : inductive -> env -> bool
+val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
 val template_polymorphic_pind : pinductive -> env -> bool
+val template_checked_ind : inductive -> env -> bool
 
 (** {5 Modules } *)
 
@@ -346,6 +352,8 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
 
 val is_polymorphic : env -> Names.GlobRef.t -> bool
 val is_template_polymorphic : env -> GlobRef.t -> bool
+val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
+val is_template_checked : env -> GlobRef.t -> bool
 val is_type_in_type : env -> GlobRef.t -> bool
 
 (** Native compiler *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c8e04b9fee..06d2e1bb21 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -236,22 +236,53 @@ let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_}
   if not ind_squashed then InType
   else Sorts.family (Sorts.sort_of_univ ind_univ)
 
+(* For a level to be template polymorphic, it must be introduced
+   by the definition (so have no constraint except lbound <= l)
+   and not to be constrained from below, so any universe l' <= l
+   can be used as an instance of l. All bounds from above, i.e.
+   l <=/< r will be valid for any l' <= l. *)
+let unbounded_from_below u cstrs =
+  Univ.Constraint.for_all (fun (l, d, r) ->
+      match d with
+      | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
+      | Lt | Le -> not (Univ.Level.equal r u))
+    cstrs
+
 (* Returns the list [x_1, ..., x_n] of levels contributing to template
-   polymorphism. The elements x_k is None if the k-th parameter (starting
-   from the most recent and ignoring let-definitions) is not contributing
-   or is Some u_k if its level is u_k and is contributing. *)
-let param_ccls paramsctxt =
+   polymorphism. The elements x_k is None if the k-th parameter
+   (starting from the most recent and ignoring let-definitions) is not
+   contributing to the inductive type's sort or is Some u_k if its level
+   is u_k and is contributing. *)
+let template_polymorphic_univs ~template_check uctx paramsctxt concl =
+  let check_level l =
+    if Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+       unbounded_from_below l (Univ.ContextSet.constraints uctx) then
+      Some l
+    else None
+  in
+  let univs = Univ.Universe.levels concl in
+  let univs =
+    if template_check then
+      Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs
+    else univs (* Doesn't check the universes can be generalized *)
+  in
   let fold acc = function
     | (LocalAssum (_, p)) ->
       (let c = Term.strip_prod_assum p in
       match kind c with
-        | Sort (Type u) -> Univ.Universe.level u
+        | Sort (Type u) ->
+          if template_check then
+            (match Univ.Universe.level u with
+             | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
+             | None -> None)
+          else Univ.Universe.level u
         | _ -> None) :: acc
     | LocalDef _ -> acc
   in
-  List.fold_left fold [] paramsctxt
+  let params = List.fold_left fold [] paramsctxt in
+  params, univs
 
-let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
   let arity = Vars.subst_univs_level_constr usubst arity in
   let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
   let indices = Vars.subst_univs_level_context usubst indices in
@@ -264,14 +295,20 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
   let ind_univ = Univ.subst_univs_level_universe usubst univ_info.ind_univ in
 
   let arity = match univ_info.ind_min_univ with
-    | None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
+    | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ}
     | Some min_univ ->
-      ((match univs with
-          | Monomorphic _ -> ()
+      let ctx = match univs with
+          | Monomorphic ctx -> ctx
           | Polymorphic _ ->
             CErrors.anomaly ~label:"polymorphic_template_ind"
-              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
-       TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
+              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
+      let param_levels, concl_levels = template_polymorphic_univs ~template_check ctx params min_univ in
+      if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+         && Univ.LSet.is_empty concl_levels then
+        CErrors.anomaly ~label:"polymorphic_template_ind"
+          Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
+      else
+        TemplateArity {template_param_levels = param_levels; template_level = min_univ}
   in
 
   let kelim = allowed_sorts univ_info in
@@ -286,10 +323,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   mind_check_names mie;
   assert (List.is_empty (Environ.rel_context env));
 
+  let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in
+
   (* universes *)
   let env_univs =
     match mie.mind_entry_universes with
-    | Monomorphic_entry ctx -> push_context_set ctx env
+    | Monomorphic_entry ctx ->
+      let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in
+      push_context_set ctx env
     | Polymorphic_entry (_, ctx) -> push_context ctx env
   in
 
@@ -335,7 +376,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
   (* Abstract universes *)
   let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
   let params = Vars.subst_univs_level_context usubst params in
-  let data = List.map (abstract_packets univs usubst params) data in
+  let template_check = Environ.check_template env in
+  let data = List.map (abstract_packets ~template_check univs usubst params) data in
 
   let env_ar_par =
     let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index aaa0d6a149..8da4e2885c 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -33,3 +33,12 @@ val typecheck_inductive : env -> mutual_inductive_entry ->
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
      Sorts.family)
     array
+
+(* Utility function to compute the actual universe parameters
+   of a template polymorphic inductive *)
+val template_polymorphic_univs :
+  template_check:bool ->
+  Univ.ContextSet.t ->
+  Constr.rel_context ->
+  Univ.Universe.t ->
+  Univ.Level.t option list * Univ.LSet.t
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 9305a91731..ccc218771a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,7 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           c', Monomorphic Univ.ContextSet.empty, cst
         | Polymorphic uctx, Some ctx ->
           let () =
-            if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
+            if not (UGraph.check_subtype ~lbound:(Environ.universes_lbound env)
+                      (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
           in
           (** Terms are compared in a context with De Bruijn universe indices *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 53f228c618..327cb2efeb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -777,7 +777,7 @@ let infer_cmp_universes env pb s0 s1 univs =
     | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
     | Set, Prop -> raise NotConvertible
     | Set, Type u -> infer_pb Univ.type0_univ u
-    | Type _u, Prop -> raise NotConvertible
+    | Type u, Prop -> infer_pb u Univ.type0m_univ
     | Type u, Set -> infer_pb u Univ.type0_univ
     | Type u0, Type u1 -> infer_pb u0 u1
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d47dc0c6e1..d22ec3b7ca 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -97,7 +97,8 @@ let check_universes error env u1 u2 =
   match u1, u2 with
   | Monomorphic _, Monomorphic _ -> env
   | Polymorphic auctx1, Polymorphic auctx2 ->
-    if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    let lbound = Environ.universes_lbound env in
+    if not (UGraph.check_subtype ~lbound (Environ.universes env) auctx2 auctx1) then
       error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
     else
       Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 6fde6e9c5f..33336079bb 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -149,10 +149,10 @@ let enforce_leq_alg u v g =
   cg
 
 exception AlreadyDeclared = G.AlreadyDeclared
-let add_universe u strict g =
+let add_universe u ~lbound ~strict g =
   let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
-  enforce_constraint (Level.set,d,u) {g with graph}
+  enforce_constraint (lbound,d,u) {g with graph}
 
 let add_universe_unconstrained u g = {g with graph=G.add u g.graph}
 
@@ -164,11 +164,11 @@ let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop k
 
 (** Subtyping of polymorphic contexts *)
 
-let check_subtype univs ctxT ctx =
+let check_subtype ~lbound univs ctxT ctx =
   if AUContext.size ctxT == AUContext.size ctx then
     let (inst, cst) = UContext.dest (AUContext.repr ctx) in
     let cstT = UContext.constraints (AUContext.repr ctxT) in
-    let push accu v = add_universe v false accu in
+    let push accu v = add_universe v ~lbound ~strict:false accu in
     let univs = Array.fold_left push univs (Instance.to_array inst) in
     let univs = merge_constraints cstT univs in
     check_constraints cst univs
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e1b5868d55..d90f01d8d1 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
 
 exception AlreadyDeclared
 
-val add_universe : Level.t -> bool -> t -> t
+val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
 
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
 val domain : t -> LSet.t
 (** Known universes *)
 
-val check_subtype : AUContext.t check_function
+val check_subtype : lbound:Level.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
 
diff --git a/library/global.ml b/library/global.ml
index 0fc9e11364..6bb4614aa4 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -119,6 +119,7 @@ let add_module_parameter mbid mte inl =
 (** Queries on the global environment *)
 
 let universes () = universes (env())
+let universes_lbound () = universes_lbound (env())
 let named_context () = named_context (env())
 let named_context_val () = named_context_val (env())
 
@@ -181,6 +182,10 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r
 
 let is_template_polymorphic r = is_template_polymorphic (env ()) r
 
+let is_template_checked r = is_template_checked (env ()) r
+
+let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r
+
 let is_type_in_type r = is_type_in_type (env ()) r
 
 let current_modpath () =
diff --git a/library/global.mli b/library/global.mli
index b089b7dd80..d0bd556d70 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -22,6 +22,7 @@ val env : unit -> Environ.env
 val env_is_initial : unit -> bool
 
 val universes : unit -> UGraph.t
+val universes_lbound : unit -> Univ.Level.t
 val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Constr.named_context
 
@@ -136,6 +137,8 @@ val is_joined_environment : unit -> bool
 
 val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
+val is_template_checked : GlobRef.t -> bool
+val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list
 val is_type_in_type : GlobRef.t -> bool
 
 (** {6 Retroknowledge } *)
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.
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f82b9cef68..b7fefca22b 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -221,14 +221,22 @@ let print_if_is_coercion ref =
 (*******************)
 (* *)
 
+let pr_template_variables = function
+  | [] -> mt ()
+  | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars
+
 let print_polymorphism ref =
   let poly = Global.is_polymorphic ref in
   let template_poly = Global.is_template_polymorphic ref in
-  [ pr_global ref ++ str " is " ++ str
-      (if poly then "universe polymorphic"
+  let template_checked = Global.is_template_checked ref in
+  let template_variables = Global.get_template_polymorphic_variables ref in
+  [ pr_global ref ++ str " is " ++
+      (if poly then str "universe polymorphic"
        else if template_poly then
-	 "template universe polymorphic"
-       else "not universe polymorphic") ]
+         (if not template_checked then str "assumed " else mt()) ++
+         str "template universe polymorphic "
+         ++ h 0 (pr_template_variables template_variables)
+       else str "not universe polymorphic") ]
 
 let print_type_in_type ref =
   let unsafe = Global.is_type_in_type ref in
diff --git a/printing/printer.ml b/printing/printer.ml
index e3225fadd5..328082fbc2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -854,6 +854,8 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism
+                                       on parameter universes has not been checked. *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
@@ -873,10 +875,13 @@ struct
         Constant.CanOrd.compare k1 k2
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
+    | TemplatePolymorphic m1, TemplatePolymorphic m2 ->
+        MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
         GlobRef.Ordered.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
+    | _, TemplatePolymorphic _ -> 1
     | _ -> -1
 
   let compare x y =
@@ -937,6 +942,9 @@ let pr_assumptionset env sigma s =
           hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded gr ->
           hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.")
+      | TemplatePolymorphic m ->
+          hov 2 (safe_pr_inductive env m ++ spc () ++
+                 strbrk"is assumed template polymorphic on all its universe parameters.")
       | TypeInType gr ->
          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
diff --git a/printing/printer.mli b/printing/printer.mli
index 788f303aee..d62d3789d3 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -192,6 +192,8 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism
+                                       on parameter universes has not been checked. *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
diff --git a/test-suite/bugs/closed/bug_9294.v b/test-suite/bugs/closed/bug_9294.v
new file mode 100644
index 0000000000..a079d672d3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9294.v
@@ -0,0 +1,29 @@
+Set Printing Universes.
+
+Inductive Foo@{i} (A:Type@{i}) : Type := foo : (Set:Type@{i}) -> Foo A.
+Arguments foo {_} _.
+Print Universes Subgraph (Foo.i).
+Definition bar : Foo True -> Set := fun '(foo x) => x.
+
+Definition foo_bar (n : Foo True) : foo (bar n) = n.
+Proof. destruct n;reflexivity. Qed.
+
+Definition bar_foo (n : Set) : bar (foo n) = n.
+Proof. reflexivity. Qed.
+
+Require Import Hurkens.
+
+Inductive box (A : Set) : Prop := Box : A -> box A.
+
+Definition Paradox : False.
+Proof.
+Fail unshelve refine (
+  NoRetractFromSmallPropositionToProp.paradox
+  (Foo True)
+  (fun A => foo A)
+  (fun A => box (bar A))
+  _
+  _
+  False
+).
+Abort.
diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v
index bc5cd0fb68..4b6916af55 100644
--- a/test-suite/coqchk/inductive_functor_template.v
+++ b/test-suite/coqchk/inductive_functor_template.v
@@ -2,7 +2,7 @@
 Module Type E. Parameter T : Type. End E.
 
 Module F (X:E).
-  #[universes(template)] Inductive foo := box : X.T -> foo.
+  Inductive foo := box : X.T -> foo.
 End F.
 
 Module ME. Definition T := nat. End ME.
diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
new file mode 100644
index 0000000000..75b2a56169
--- /dev/null
+++ b/test-suite/failure/Template.v
@@ -0,0 +1,32 @@
+(*
+Module TestUnsetTemplateCheck.
+  Unset Template Check.
+
+  Section Foo.
+
+    Context (A : Type).
+
+    Definition cstr := nat : ltac:(let ty := type of A in exact ty).
+
+    Inductive myind :=
+    | cons : A -> myind.
+  End Foo.
+
+  (* Can only succeed if no template check is performed *)
+  Check myind True : Prop.
+
+  Print Assumptions myind.
+  (*
+  Axioms:
+  myind is template polymorphic on all its universe parameters.
+   *)
+  About myind.
+(*
+myind : Type@{Top.60} -> Type@{Top.60}
+
+myind is assumed template universe polymorphic on Top.60
+Argument scope is [type_scope]
+Expands to: Inductive Top.TestUnsetTemplateCheck.myind
+*)
+End TestUnsetTemplateCheck.
+*)
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4e949dcb04..a040b69b44 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -84,7 +84,6 @@ Print f.
 (* Was enhancement request #5142 (error message reported on the most
    general return clause heuristic) *)
 
-#[universes(template)]
 Inductive gadt : Type -> Type :=
 | gadtNat : nat -> gadt nat
 | gadtTy : forall T, T -> gadt T.
diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v
index 6976f35a88..0e84bf3966 100644
--- a/test-suite/output/Coercions.v
+++ b/test-suite/output/Coercions.v
@@ -1,7 +1,7 @@
 (* Submitted by Randy Pollack *)
 
-#[universes(template)] Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
-#[universes(template)] Record rel (S : Set) : Type :=  {sr_rel :> S -> S -> Prop}.
+Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
+Record rel (S : Set) : Type :=  {sr_rel :> S -> S -> Prop}.
 
 Section testSection.
 Variables (S : Set) (P : pred S) (R : rel S) (x : S).
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index f9398fdca9..1ecd9771eb 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -101,7 +101,7 @@ Section decoder_result.
 
  Variable inst : Type.
 
- #[universes(template)] Inductive decoder_result : Type :=
+ Inductive decoder_result : Type :=
  | DecUndefined : decoder_result
  | DecUnpredictable : decoder_result
  | DecInst : inst -> decoder_result
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 9b25c2dbd3..61ae4edbd1 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
   omega.
 Qed.
 
-#[universes(template)] CoInductive Inf := S { projS : Inf }.
+CoInductive Inf := S { projS : Inf }.
 Definition expand_Inf (x : Inf) := S (projS x).
 CoFixpoint inf := S inf.
 Eval compute in inf.
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 29614c032a..aeebc0f98b 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
 (**********************************************************************)
 (* Test printing of #4932                                             *)
 
-#[universes(template)] Inductive ftele : Type :=
+Inductive ftele : Type :=
 | fb {T:Type} : T -> ftele
 | fr {T} : (T -> ftele) -> ftele.
 
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 0c1b08f5a3..d671053c07 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -53,7 +53,7 @@ Module Suboptimal.
 (** This test shows an example which exposes the [let] introduced by
     the pattern notation in binders. *)
 
-#[universes(template)] Inductive Fin (n:nat) := Z : Fin n.
+Inductive Fin (n:nat) := Z : Fin n.
 Definition F '(n,p) : Type := (Fin n * Fin p)%type.
 Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
 Print both_z.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ab4172711e..e788977fb7 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,6 +1,6 @@
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
-existT is template universe polymorphic
+existT is template universe polymorphic on sigT.u0 sigT.u1
 Argument A is implicit
 Argument scopes are [type_scope function_scope _ _]
 Expands to: Constructor Coq.Init.Specif.existT
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 35f36e87d7..14d63d39c4 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -6,7 +6,7 @@ Class HostFunction := host_func : Type.
 
 Section store.
   Context `{HostFunction}.
-  #[universes(template)] Record store := { store_funcs : host_func }.
+  Record store := { store_funcs : host_func }.
 End store.
 
 Check (fun (S:@store nat) => S.(store_funcs)).
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 4fe7b051f8..d9a649fadc 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,12 +20,12 @@ Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
 
-#[universes(template)] Record N := C { T : Type; _ : True }.
+Record N := C { T : Type; _ : True }.
 Check fun x:N => let 'C _ p := x in p.
 Check fun x:N => let 'C T _ := x in T.
 Check fun x:N => let 'C T p := x in (T,p).
 
-#[universes(template)] Record M := D { U : Type; a := 0; q : True }.
+Record M := D { U : Type; a := 0; q : True }.
 Check fun x:M => let 'D T _ p := x in p.
 Check fun x:M => let 'D T _ p := x in T.
 Check fun x:M => let 'D T p := x in (T,p).
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
index 99183f2064..9cf6ad35b8 100644
--- a/test-suite/output/ShowMatch.v
+++ b/test-suite/output/ShowMatch.v
@@ -3,12 +3,12 @@
 *)
 
 Module A.
-  #[universes(template)] Inductive foo := f.
+  Inductive foo := f.
   Show Match foo. (* no need to disambiguate *)
 End A. 
 
 Module B.
-  #[universes(template)] Inductive foo := f.
+  Inductive foo := f.
   (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
   Show Match A.foo. 
 End B.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 222a808768..a89fd64999 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -68,9 +68,9 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 bobmorane = 
-let tt := Type@{UnivBinders.32} in
-let ff := Type@{UnivBinders.34} in tt -> ff
-     : Type@{max(UnivBinders.31,UnivBinders.33)}
+let tt := Type@{UnivBinders.33} in
+let ff := Type@{UnivBinders.35} in tt -> ff
+     : Type@{max(UnivBinders.32,UnivBinders.34)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
@@ -143,16 +143,16 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.56 UnivBinders.57} :
-Type@{UnivBinders.56} -> Type@{i}
-(* i UnivBinders.56 UnivBinders.57 |=  *)
+axfoo@{i UnivBinders.57 UnivBinders.58} :
+Type@{UnivBinders.57} -> Type@{i}
+(* i UnivBinders.57 UnivBinders.58 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.56 UnivBinders.57} :
-Type@{UnivBinders.57} -> Type@{i}
-(* i UnivBinders.56 UnivBinders.57 |=  *)
+axbar@{i UnivBinders.57 UnivBinders.58} :
+Type@{UnivBinders.58} -> Type@{i}
+(* i UnivBinders.57 UnivBinders.58 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
index 0eb5db1733..7465442cab 100644
--- a/test-suite/output/Warnings.v
+++ b/test-suite/output/Warnings.v
@@ -1,5 +1,5 @@
 (* Term in warning was not printed in the right environment at some time *)
-#[universes(template)] Record A := { B:Type; b:B->B }.
+Record A := { B:Type; b:B->B }.
 Definition a B := {| B:=B; b:=fun x => x |}.
 Canonical Structure a.
 
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 209fedc343..57a4739e9f 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -21,6 +21,6 @@ Print P.
 
 (* Note: exact numbers of evars are not important... *)
 
-#[universes(template)] Inductive T (n:nat) : Type := A : T n.
+Inductive T (n:nat) : Type := A : T n.
 Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index cfc25c3346..656362b8fc 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -46,3 +46,129 @@ Module No.
   Definition j_lebox (A:Type@{j}) := Box A.
   Fail Definition box_lti A := Box A : Type@{i}.
 End No.
+
+Module DefaultProp.
+  Inductive identity (A : Type) (a : A) : A -> Type := id_refl : identity A a a.
+
+  (* By default template polymorphism does not interact with inductives
+     which naturally fall in Prop *)
+  Check (identity nat 0 0 : Prop).
+End DefaultProp.
+
+Module ExplicitTemplate.
+  #[universes(template)]
+  Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a.
+
+  (* Weird interaction of template polymorphism and inductive types
+     which naturally fall in Prop: this one is template polymorphic but not on i:
+     it just lives in any universe *)
+  Check (identity Type nat nat : Prop).
+End ExplicitTemplate.
+
+Polymorphic Definition f@{i} : Type@{i} := nat.
+Polymorphic Definition baz@{i} : Type@{i} -> Type@{i} := fun x => x.
+
+Section Foo.
+  Universe u.
+  Context (A : Type@{u}).
+
+  Inductive Bar :=
+  | bar : A -> Bar.
+
+  Set Universe Minimization ToSet.
+  Inductive Baz :=
+  | cbaz : A -> baz Baz -> Baz.
+
+  Inductive Baz' :=
+  | cbaz' : A -> baz@{Set} nat -> Baz'.
+
+  (* 2 constructors, at least in Set *)
+  Inductive Bazset@{v} :=
+  | cbaz1 : A -> baz@{v} Bazset -> Bazset
+  | cbaz2 : Bazset.
+
+  Eval compute in ltac:(let T := type of A in exact T).
+
+  Inductive Foo : Type :=
+  | foo : A -> f -> Foo.
+
+End Foo.
+
+Set Printing Universes.
+(* Cannot fall back to Prop or Set anymore as baz is no longer template-polymorphic *)
+Fail Check Bar True : Prop.
+Fail Check Bar nat : Set.
+About Baz.
+
+Check cbaz True I.
+
+(** Neither can it be Set *)
+Fail Check Baz nat : Set.
+
+(** No longer possible for Baz' which contains a type in Set *)
+Fail Check Baz' True : Prop.
+Fail Check Baz' nat : Set.
+
+Fail Check Bazset True : Prop.
+Fail Check Bazset True : Set.
+
+(** We can force the universe instantiated in [baz Bazset] to be [u], so Bazset lives in max(Set, u). *)
+Constraint u = Bazset.v.
+(** As u is global it is already > Set, so: *)
+Definition bazsetex@{i | i < u} : Type@{u} := Bazset Type@{i}.
+
+(* Bazset is closed for universes u = u0, cannot be instantiated with Prop *)
+Definition bazseetpar (X : Type@{u}) : Type@{u} := Bazset X.
+
+(** Would otherwise break singleton elimination and extraction. *)
+Fail Check Foo True : Prop.
+Fail Check Foo True : Set.
+
+Definition foo_proj {A} (f : Foo A) : nat :=
+  match f with foo _ _ n => n end.
+
+Definition ex : Foo True := foo _ I 0.
+Check foo_proj ex.
+
+(** See failure/Template.v for a test of the unsafe Unset Template Check usage *)
+
+Module AutoTemplateTest.
+Set Warnings "+auto-template".
+Section Foo.
+  Universe u'.
+  Context (A : Type@{u'}).
+
+  (* Not failing as Bar cannot be made template polymorphic at all *)
+  Inductive Bar :=
+  | bar : A -> Bar.
+End Foo.
+End AutoTemplateTest.
+
+Module TestTemplateAttribute.
+  Section Foo.
+    Universe u.
+    Context (A : Type@{u}).
+
+    (* Failing as Bar cannot be made template polymorphic at all *)
+    Fail #[universes(template)] Inductive Bar :=
+    | bar : A -> Bar.
+
+  End Foo.
+End TestTemplateAttribute.
+
+Module SharingWithoutSection.
+Inductive Foo A (S:= fun _ => Set : ltac:(let ty := type of A in exact ty))
+  := foo : S A -> Foo A.
+Fail Check Foo True : Prop.
+End SharingWithoutSection.
+
+Module OkNotCovered.
+(* Here it happens that box is safe but we don't see it *)
+Section S.
+Universe u.
+Variable A : Type@{u}.
+Inductive box (A:Type@{u}) := Box : A -> box A.
+Definition B := Set : Type@{u}.
+End S.
+Fail Check box True : Prop.
+End OkNotCovered.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 428af5fcfe..69bd1e6c96 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -286,7 +286,6 @@ Local Open Scope list_scope.
 (** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
 (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *)
-#[universes(template)]
 Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist.
 Local Infix "::" := Tcons.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 071810acdc..6858706cb3 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -27,7 +27,6 @@ Require Export Coq.Classes.Morphisms.
 
 (** A setoid wraps an equivalence. *)
 
-#[universes(template)]
 Class Setoid A := {
   equiv : relation A ;
   setoid_equiv :> Equivalence equiv }.
@@ -129,7 +128,6 @@ Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (
 
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
 
-#[universes(template)]
 Class PartialSetoid (A : Type) :=
   { pequiv : relation A ; pequiv_prf :> PER pequiv }.
 
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index 5025bce093..274cb4afd3 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -14,3 +14,6 @@ Local Set Warnings "-deprecated".
 Require Export Coq.Compat.Coq810.
 
 Unset Private Polymorphic Universes.
+
+(** Unsafe flag, can hide inconsistencies. *)
+Global Unset Template Check.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 801be79ba4..8627ff7353 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -45,20 +45,23 @@ Hint Transparent key : core.
 
 (** * Trees *)
 
-Section Elt.
-
-Variable elt : Type.
-
 (** * Trees
 
    The fifth field of [Node] is the height of the tree *)
 
 #[universes(template)]
-Inductive tree :=
+Inductive tree {elt : Type} :=
   | Leaf : tree
   | Node : tree -> key -> elt -> tree -> int -> tree.
+Arguments tree : clear implicits.
 
-Notation t := tree.
+Section Elt.
+
+Variable elt : Type.
+
+Notation t := (tree elt).
+
+Implicit Types m : t.
 
 (** * Basic functions on trees: height and cardinal *)
 
@@ -76,7 +79,7 @@ Fixpoint cardinal (m : t) : nat :=
 
 (** * Empty Map *)
 
-Definition empty := Leaf.
+Definition empty : t := Leaf.
 
 (** * Emptyness test *)
 
@@ -236,7 +239,6 @@ Fixpoint join l : key -> elt -> t -> t :=
     - [o] is the result of [find x m].
 *)
 
-#[universes(template)]
 Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }.
 Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
 
@@ -293,7 +295,6 @@ Variable cmp : elt->elt->bool.
 
 (** ** Enumeration of the elements of a tree *)
 
-#[universes(template)]
 Inductive enumeration :=
  | End : enumeration
  | More : key -> elt -> t -> enumeration -> enumeration.
@@ -338,6 +339,9 @@ Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End).
 
 End Elt.
 Notation t := tree.
+Arguments Leaf : clear implicits.
+Arguments Node [elt].
+
 Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
 Notation "t #l" := (t_left t) (at level 9, format "t '#l'").
 Notation "t #o" := (t_opt t) (at level 9, format "t '#o'").
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 2af6e5c6a4..b21d809059 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -1024,7 +1024,6 @@ Module E := X.
 
 Definition key := E.t.
 
-#[universes(template)]
 Record slist (elt:Type) :=
   {this :> Raw.t elt; sorted : sort (@Raw.PX.ltk elt) this}.
 Definition t (elt:Type) : Type := slist elt.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0c04437581..b9a8b0a73d 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -868,8 +868,6 @@ Module Make (X: DecidableType) <: WS with Module E:=X.
 
  Module E := X.
  Definition key := E.t.
-
-#[universes(template)]
  Record slist (elt:Type) :=
   {this :> Raw.t elt; NoDup : NoDupA (@Raw.PX.eqk elt) this}.
  Definition t (elt:Type) := slist elt.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 1639115cbd..3e0bf1d8ae 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -387,8 +387,10 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined.
 (** [identity A a] is the family of datatypes on [A] whose sole non-empty
     member is the singleton datatype [identity A a a] whose
     sole inhabitant is denoted [identity_refl A a] *)
+(** Beware: this inductive actually falls into [Prop], as the sole
+    constructor has no arguments and [-indices-matter] is not
+    activated in the standard library. *)
 
-#[universes(template)]
 Inductive identity (A:Type) (a:A) : A -> Type :=
   identity_refl : identity a a.
 Hint Resolve identity_refl: core.
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index c11a0941fa..4c6520feb3 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -73,14 +73,17 @@ End MemoFunction.
     reused thanks to a temporary hiding of the dependency
     in a "container" [memo_val]. *)
 
+#[universes(template)]
+Inductive memo_val {A : nat -> Type} : Type :=
+  memo_mval: forall n, A n -> memo_val.
+Arguments memo_val : clear implicits.
+
 Section DependentMemoFunction.
 
 Variable A: nat -> Type.
 Variable f: forall n, A n.
 
-#[universes(template)]
-Inductive memo_val: Type :=
-  memo_mval: forall n, A n -> memo_val.
+Notation memo_val := (memo_val A).
 
 Fixpoint is_eq (n m : nat) : {n = m} + {True} :=
   match n, m return {n = m} + {True} with
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 407a7ae45d..0daae0391c 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -12,13 +12,13 @@ Set Implicit Arguments.
 
 (** Streams *)
 
-Section Streams.
+CoInductive Stream (A : Type) :=
+  Cons : A -> Stream A -> Stream A.
 
-Variable A : Type.
+Section Streams.
+  Variable A : Type.
 
-#[universes(template)]
-CoInductive Stream : Type :=
-    Cons : A -> Stream -> Stream.
+  Notation Stream := (Stream A).
 
 
 Definition hd (x:Stream) := match x with
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 4442108ffc..8a71158f4c 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -208,7 +208,6 @@ Definition concat s1 s2 :=
     - [present] is [true] if and only if [s] contains  [x].
 *)
 
-#[universes(template)]
 Record triple := mktriple { t_left:t; t_in:bool; t_right:t }.
 Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
 
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 37a169b02e..bf6336ae47 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -48,7 +48,6 @@ Module Type Ops (X:OrderedType)(Info:InfoTyp).
 Definition elt := X.t.
 Hint Transparent elt : core.
 
-#[universes(template)]
 Inductive tree  : Type :=
 | Leaf : tree
 | Node : Info.t -> tree -> X.t -> tree -> tree.
@@ -168,7 +167,6 @@ end.
 (** Enumeration of the elements of a tree. This corresponds
     to the "samefringe" notion in the literature. *)
 
-#[universes(template)]
 Inductive enumeration :=
  | End : enumeration
  | More : elt -> tree -> enumeration -> enumeration.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 29c84d0d1a..33f6b1050c 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -439,7 +439,6 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
 
  Definition elt := E.t.
 
-#[universes(template)]
  Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
  Definition t := t_.
  Arguments Mkt this {is_ok}.
diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v
index 83e9c29b13..6e08378df4 100644
--- a/theories/Numbers/Cyclic/Abstract/DoubleType.v
+++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v
@@ -18,46 +18,34 @@ Local Open Scope Z_scope.
 Definition base digits := Z.pow 2 (Zpos digits).
 Arguments base digits: simpl never.
 
-Section Carry.
+#[universes(template)]
+Variant carry (A : Type) :=
+| C0 : A -> carry A
+| C1 : A -> carry A.
 
- Variable A : Type.
-
- #[universes(template)]
- Variant carry :=
-  | C0 : A -> carry
-  | C1 : A -> carry.
-
- Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c :=
+Definition interp_carry {A} (sign:Z)(B:Z)(interp:A -> Z) c :=
   match c with
   | C0 x => interp x
   | C1 x => sign*B + interp x
   end.
 
-End Carry.
-
-Section Zn2Z.
-
- Variable znz : Type.
-
- (** From a type [znz] representing a cyclic structure Z/nZ,
-     we produce a representation of Z/2nZ by pairs of elements of [znz]
-     (plus a special case for zero). High half of the new number comes
-     first.
+(** From a type [znz] representing a cyclic structure Z/nZ,
+    we produce a representation of Z/2nZ by pairs of elements of [znz]
+    (plus a special case for zero). High half of the new number comes
+    first.
  *)
+#[universes(template)]
+Variant zn2z {znz : Type} :=
+| W0 : zn2z
+| WW : znz -> znz -> zn2z.
+Arguments zn2z : clear implicits.
 
- #[universes(template)]
- Variant zn2z :=
-  | W0 : zn2z
-  | WW : znz -> znz -> zn2z.
-
- Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) :=
+Definition zn2z_to_Z znz (wB:Z) (w_to_Z:znz->Z) (x:zn2z znz) :=
   match x with
   | W0 => 0
   | WW xh xl => w_to_Z xh * wB + w_to_Z xl
   end.
 
-End Zn2Z.
-
 Arguments W0 {znz}.
 
 (** From a cyclic representation [w], we iterate the [zn2z] construct
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 128ee286b8..6da0fe3966 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -137,7 +137,6 @@ Definition IsStepFun (f:R -> R) (a b:R) : Type :=
   { l:Rlist & is_subdivision f a b l }.
 
 (** ** Class of step functions *)
-#[universes(template)]
 Record StepFun (a b:R) : Type := mkStepFun
   {fe :> R -> R; pre : IsStepFun fe a b}.
 
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 5443ff68ed..c94a373ca0 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -116,7 +116,6 @@ Qed.
 (*******************************)
 
 (*********)
-#[universes(template)]
 Record Metric_Space : Type :=
   {Base : Type;
     dist : Base -> Base -> R;
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index cfcc82d765..d21042884e 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -380,7 +380,6 @@ Proof.
   apply Rinv_0_lt_compat; prove_sup0.
 Qed.
 
-#[universes(template)]
 Record family : Type := mkfamily
   {ind : R -> Prop;
     f :> R -> R -> Prop;
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index e1d7d37e42..745db25a54 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -100,11 +100,9 @@ Hint Resolve Totally_ordered_definition Upper_Bound_definition
 Section Specific_orders.
   Variable U : Type.
 
-  #[universes(template)]
   Record Cpo : Type := Definition_of_cpo
     {PO_of_cpo : PO U; Cpo_cond : Complete U PO_of_cpo}.
 
-  #[universes(template)]
   Record Chain : Type := Definition_of_chain
     {PO_of_chain : PO U;
     Chain_cond : Totally_ordered U PO_of_chain (@Carrier_of _ PO_of_chain)}.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index e9233a34e7..6aefcf32c0 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -22,7 +22,6 @@ Section multiset_defs.
   Hypothesis eqA_equiv : Equivalence eqA.
   Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
-  #[universes(template)]
   Inductive multiset : Type :=
     Bag : (A -> nat) -> multiset.
 
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index d2fae6db28..e23d9c2f55 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -36,7 +36,6 @@ Section Partial_orders.
 
   Definition Rel := Relation U.
 
-  #[universes(template)]
   Record PO : Type := Definition_of_PO
     { Carrier_of : Ensemble U;
       Rel_of : Relation U;
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 76e555ed5a..48a852052e 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -42,7 +42,6 @@ Section defs.
   Let emptyBag := EmptyBag A.
   Let singletonBag := SingletonBag _ eqA_dec.
 
-  #[universes(template)]
   Inductive Tree :=
     | Tree_Leaf : Tree
     | Tree_Node : A -> Tree -> Tree -> Tree.
@@ -129,8 +128,7 @@ Section defs.
 
   (** ** Merging two sorted lists *)
 
-  #[universes(template)]
-  Inductive merge_lem (l1 l2:list A) : Type :=
+   Inductive merge_lem (l1 l2:list A) : Type :=
     merge_exist :
     forall l:list A,
       Sorted leA l ->
@@ -203,7 +201,6 @@ Section defs.
 
   (** ** Specification of heap insertion *)
 
-  #[universes(template)]
   Inductive insert_spec (a:A) (T:Tree) : Type :=
     insert_exist :
     forall T1:Tree,
@@ -237,7 +234,6 @@ Section defs.
 
   (** ** Building a heap from a list *)
 
-  #[universes(template)]
   Inductive build_heap (l:list A) : Type :=
     heap_exist :
     forall T:Tree,
@@ -262,7 +258,6 @@ Section defs.
 
   (** ** Building the sorted list *)
 
-  #[universes(template)]
   Inductive flat_spec (T:Tree) : Type :=
     flat_exist :
     forall l:list A,
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index d747258f56..6ddbc8e214 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -14,17 +14,18 @@
 
 Require Import Eqdep.
 
+#[universes(template)]
+Inductive WO (A : Type) (B : A -> Type) : Type :=
+  sup : forall (a:A) (f:B a -> WO A B), WO A B.
+
 Section WellOrdering.
   Variable A : Type.
   Variable B : A -> Type.
 
-  #[universes(template)]
-  Inductive WO : Type :=
-    sup : forall (a:A) (f:B a -> WO), WO.
-
+  Notation WO := (WO A B).
 
   Inductive le_WO : WO -> WO -> Prop :=
-    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f).
+    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup _ _ a f).
 
   Theorem wf_WO : well_founded le_WO.
   Proof.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 577544f971..fee928430c 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -212,7 +212,6 @@ Module MoreInt (Import I:Int).
     | EZofI : ExprI -> ExprZ
     | EZraw : Z -> ExprZ.
 
-  #[universes(template)]
   Inductive ExprP : Type :=
     | EPeq : ExprZ -> ExprZ -> ExprP
     | EPlt : ExprZ -> ExprZ -> ExprP
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 64c1da20b6..0490c35970 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -32,6 +32,10 @@ let set_type_in_type () =
   let typing_flags = Environ.typing_flags (Global.env ()) in
   Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
 
+let set_no_template_check () =
+  let typing_flags = Environ.typing_flags (Global.env ()) in
+  Global.set_typing_flags { typing_flags with Declarations.check_template = false }
+
 (******************************************************************************)
 
 type color = [`ON | `AUTO | `EMACS | `OFF]
@@ -525,6 +529,7 @@ let parse_args ~help ~init arglist : t * string list =
     |"-list-tags" -> set_query oval PrintTags
     |"-time" -> { oval with config = { oval.config with time = true }}
     |"-type-in-type" -> set_type_in_type (); oval
+    |"-no-template-check" -> set_no_template_check (); oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
     |"-where" -> set_query oval PrintWhere
     |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index cdb2e36fbd..8555d78156 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -82,6 +82,7 @@ let print_usage_common co command =
 \n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
+\n  -no-template-check     disable checking of universes constraints on universes parameterizing template polymorphic inductive types\
 \n  -mangle-names x        mangle auto-generated names using prefix x\
 \n  -set \"Foo Bar\"         enable Foo Bar (as Set Foo Bar. in a file)\
 \n  -set \"Foo Bar=value\"   set Foo Bar to value (value is interpreted according to Foo Bar's type)\
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index a72e43de01..cb034bdff6 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -353,6 +353,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
       in
-      accu
-
+      if not mind.mind_typing_flags.check_template then
+        let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+        ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu
+      else accu
   in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index d414d57c0d..98fe436a22 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -345,7 +345,7 @@ let build_beq_scheme mode kn =
           Vars.substl subst cores.(i)
         in
         create_input fix),
-       UState.make (Global.universes ())),
+       UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())),
       !eff
 
 let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
@@ -690,7 +690,7 @@ let make_bl_scheme mode mind =
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
-  let ctx = UState.make (Global.universes ()) in
+  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal
@@ -820,7 +820,7 @@ let make_lb_scheme mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
-  let ctx = UState.make (Global.universes ()) in
+  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal
@@ -996,7 +996,7 @@ let make_eq_decidability mode mind =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let u = Univ.Instance.empty in
-  let ctx = UState.make (Global.universes ()) in
+  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index adbe196699..98b869d72e 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -114,20 +114,22 @@ let mk_mltype_data sigma env assums arity indname =
     inductives which are recognized when a "Type" appears at the end of the conlusion in
     the source syntax. *)
 
-let rec check_anonymous_type ind =
+let rec check_type_conclusion ind =
   let open Glob_term in
     match DAst.get ind with
-    | GSort (UAnonymous {rigid=true}) -> true
+    | GSort (UAnonymous {rigid=true}) -> (Some true)
+    | GSort (UNamed _) -> (Some false)
     | GProd ( _, _, _, e)
     | GLetIn (_, _, _, e)
     | GLambda (_, _, _, e)
     | GApp (e, _)
-    | GCast (e, _) -> check_anonymous_type e
-    | _ -> false
+    | GCast (e, _) -> check_type_conclusion e
+    | _ -> None
 
-let make_conclusion_flexible sigma = function
+let make_anonymous_conclusion_flexible sigma = function
   | None -> sigma
-  | Some s ->
+  | Some (false, _) -> sigma
+  | Some (true, s) ->
     (match EConstr.ESorts.kind sigma s with
      | Type u ->
        (match Univ.universe_level u with
@@ -136,17 +138,23 @@ let make_conclusion_flexible sigma = function
         | None -> sigma)
      | _ -> sigma)
 
-let interp_ind_arity env sigma ind =
+let intern_ind_arity env sigma ind =
   let c = intern_gen IsType env sigma ind.ind_arity in
   let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
+  let pseudo_poly = check_type_conclusion c in
+  (constr_loc ind.ind_arity, c, impls, pseudo_poly)
+
+let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) =
   let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
-  let pseudo_poly = check_anonymous_type c in
   match Reductionops.sort_of_arity env sigma t with
   | exception Invalid_argument _ ->
-    user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
+    user_err ?loc (str "Not an arity")
   | s ->
-    let concl = if pseudo_poly then Some s else None in
-    sigma, (t, Retyping.relevance_of_sort s,  concl, impls)
+    let concl = match pseudo_poly with
+      | Some b -> Some (b, s)
+      | None -> None
+    in
+    sigma, (t, Retyping.relevance_of_sort s, concl, impls)
 
 let interp_cstrs env sigma impls mldata arity ind =
   let cnames,ctyps = List.split ind.ind_lc in
@@ -251,7 +259,7 @@ let solve_constraints_system levels level_bounds =
   done;
   v
 
-let inductive_levels env evd poly arities inds =
+let inductive_levels env evd arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
     if Sorts.is_prop a || Sorts.is_sprop a then None
@@ -286,7 +294,7 @@ let inductive_levels env evd poly arities inds =
     CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
       if is_impredicative_sort env du then
         (* Any product is allowed here. *)
-        evd, arity :: arities
+        evd, (false, arity) :: arities
       else (* If in a predicative sort, or asked to infer the type,
               we take the max of:
               - indices (if in indices-matter mode)
@@ -300,7 +308,6 @@ let inductive_levels env evd poly arities inds =
               raise (InductiveError LargeNonPropInductiveNotInType)
             else evd
           else evd
-            (* Evd.set_leq_sort env evd (Type cu) du *)
         in
         let evd =
           if len >= 2 && Univ.is_type0m_univ cu then
@@ -311,14 +318,14 @@ let inductive_levels env evd poly arities inds =
           else evd
         in
         let duu = Sorts.univ_of_sort du in
-        let evd =
+        let template_prop, evd =
           if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
             if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
-              Evd.set_eq_sort env evd Sorts.prop du
-            else evd
-          else Evd.set_eq_sort env evd (sort_of_univ cu) du
+              true, Evd.set_eq_sort env evd Sorts.prop du
+            else false, evd
+          else false, Evd.set_eq_sort env evd (sort_of_univ cu) du
         in
-          (evd, arity :: arities))
+          (evd, (template_prop, arity) :: arities))
     (evd,[]) (Array.to_list levels') destarities sizes
   in evd, List.rev arities
 
@@ -328,6 +335,17 @@ let check_named {CAst.loc;v=na} = match na with
   let msg = str "Parameters must be named." in
   user_err ?loc  msg
 
+let template_polymorphism_candidate env uctx params concl =
+  match uctx with
+  | Entries.Monomorphic_entry uctx ->
+    let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
+    if not concltemplate then false
+    else
+      let template_check = Environ.check_template env in
+      let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
+      let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in
+      not (template_check && Univ.LSet.is_empty conclunivs)
+  | Entries.Polymorphic_entry _ -> false
 
 let check_param = function
 | CLocalDef (na, _, _) -> check_named na
@@ -345,25 +363,46 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
-let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
-  check_all_names_different indl;
-  List.iter check_param paramsl;
-  if not (List.is_empty uparamsl) && not (List.is_empty notations)
-  then user_err (str "Inductives with uniform parameters may not have attached notations.");
-  let sigma, udecl = interp_univ_decl_opt env0 udecl in
+let interp_params env udecl uparamsl paramsl =
+  let sigma, udecl = interp_univ_decl_opt env udecl in
   let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
-    interp_context_evars ~program_mode:false env0 sigma uparamsl in
+    interp_context_evars ~program_mode:false env sigma uparamsl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
     interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl
   in
-  let indnames = List.map (fun ind -> ind.ind_name) indl in
-
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter is_local_assum ctx_params in
-  let params = List.map (RelDecl.get_name %> Name.get_id) assums in
+  sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
+  List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl)
+
+let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
+  check_all_names_different indl;
+  List.iter check_param paramsl;
+  if not (List.is_empty uparamsl) && not (List.is_empty notations)
+  then user_err (str "Inductives with uniform parameters may not have attached notations.");
+
+  let indnames = List.map (fun ind -> ind.ind_name) indl in
+  let sigma, env_params, infos =
+    interp_params env0 udecl uparamsl paramsl
+  in
 
   (* Interpret the arities *)
-  let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
+  let arities = List.map (intern_ind_arity env_params sigma) indl in
+
+  let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template =
+    let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in
+    if not poly && is_template then
+      (* In case of template polymorphism, we need to compute more constraints *)
+      let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in
+      let sigma, env_params, infos =
+        interp_params env0 udecl uparamsl paramsl
+      in
+      let arities = List.map (intern_ind_arity env_params sigma) indl in
+      sigma, env_params, infos, arities, is_template
+    else sigma, env_params, infos, arities, is_template
+  in
+
+  let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in
   let arities, relevances, arityconcl, indimpls = List.split4 arities in
 
   let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
@@ -410,31 +449,36 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let nf = Evarutil.nf_evars_universes sigma in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
-  let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in
-  let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
+  let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
+  let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
-  let arities = List.map nf arities in
+  let arities = List.map (fun (template, arity) -> template, nf arity) arities in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
-  let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in
-  let sigma = restrict_inductive_universes sigma ctx_params arities constructors in
+  let arityconcl = List.map (Option.map (fun (anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
+  let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
   let uctx = Evd.check_univ_decl ~poly sigma udecl in
-  List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
+  List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities;
   Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
     List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
     constructors;
 
   (* Build the inductive entries *)
-  let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) ->
+  let entries = List.map4 (fun ind (templatearity, arity) concl (cnames,ctypes,cimpls) ->
+      let template_candidate () =
+        templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in
       let template = match template with
         | Some template ->
-          if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+          if poly && template then user_err
+              Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.");
+          if template && not (template_candidate ()) then
+            user_err Pp.(strbrk "Inductive " ++ Id.print ind.ind_name ++
+                         str" cannot be made template polymorphic.");
           template
         | None ->
-          should_auto_template ind.ind_name (not poly &&
-          Option.cata (fun s -> not (Sorts.is_small s)) false concl)
+          should_auto_template ind.ind_name (template_candidate ())
       in
       { mind_entry_typename = ind.ind_name;
         mind_entry_arity = arity;
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 285be8cd51..7587bd165f 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -62,3 +62,17 @@ val should_auto_template : Id.t -> bool -> bool
 (** [should_auto_template x b] is [true] when [b] is [true] and we
    automatically use template polymorphism. [x] is the name of the
    inductive under consideration. *)
+
+val template_polymorphism_candidate :
+  Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool
+(** [template_polymorphism_candidate env uctx params conclsort] is
+   [true] iff an inductive with params [params] and conclusion
+   [conclsort] would be definable as template polymorphic.  It should
+   have at least one universe in its monomorphic universe context that
+   can be made parametric in its conclusion sort, if one is given.
+   If the [Template Check] flag is false we just check that the conclusion sort
+   is not small. *)
+
+val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t
+(** [sign_level env sigma ctx] computes the universe level of the context [ctx]
+    as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *)
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index e3cffa8523..8fd6bc7eab 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -530,7 +530,7 @@ let obligation_terminator entries uctx { name; num; auto } =
            declares the univs of the constant,
            each subsequent obligation declares its own additional
            universes and constraints if any *)
-        if defined then UState.make (Global.universes ())
+        if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
         else ctx
     in
     let prg = {prg with prg_ctx} in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5d153fa8be..da14b6e979 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -454,7 +454,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ }
     if not prg.prg_poly (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
-      let ctx = UState.make (Global.universes ()) in
+      let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
       let ctx' = UState.merge_subst ctx (UState.subst ctx') in
       Univ.Instance.empty, ctx'
     else
diff --git a/vernac/record.ml b/vernac/record.ml
index 11237f3873..831fb53549 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -85,10 +85,10 @@ let interp_fields_evars env sigma impls_env nots l =
 
 let compute_constructor_level evars env l =
   List.fold_right (fun d (env, univ) ->
-    let univ = 
+    let univ =
       if is_local_assum d then
 	let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
-	  Univ.sup (univ_of_sort s) univ 
+          Univ.sup (univ_of_sort s) univ
       else univ
     in (EConstr.push_rel d env, univ))
     l (env, Univ.Universe.sprop)
@@ -101,8 +101,19 @@ let binder_of_decl = function
 
 let binders_of_decls = List.map binder_of_decl
 
+let check_anonymous_type ind =
+  match ind with
+  | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
+  | _ -> false
+
 let typecheck_params_and_fields finite def poly pl ps records =
   let env0 = Global.env () in
+  (* Special case elaboration for template-polymorphic inductives,
+     lower bound on introduced universes is Prop so that we do not miss
+     any Set <= i constraint for universes that might actually be instantiated with Prop. *)
+  let is_template =
+    List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
+  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
   let () =
     let error bk {CAst.loc; v=name} =
@@ -111,15 +122,15 @@ let typecheck_params_and_fields finite def poly pl ps records =
         user_err ?loc ~hdr:"record" (str "Record parameters must be named")
       | _ -> ()
     in
-      List.iter 
+      List.iter
 	(function CLocalDef (b, _, _) -> error default_binder_kind b
 	   | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
            | CLocalPattern {CAst.loc} ->
               Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
-  in 
+  in
   let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in
   let fold (sigma, template) (_, t, _, _) = match t with
-    | Some t -> 
+    | Some t ->
        let env = EConstr.push_rel_context newps env0 in
        let poly =
          match t with
@@ -138,7 +149,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
                  (sigma, false), (s, s')
              else (sigma, false), (s, s'))
 	 | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
-    | None -> 
+    | None ->
       let uvarkind = Evd.univ_flexible_alg in
       let sigma, s = Evd.new_sort_variable uvarkind sigma in
       (sigma, template), (EConstr.mkSort s, s)
@@ -168,23 +179,23 @@ let typecheck_params_and_fields finite def poly pl ps records =
     let _, univ = compute_constructor_level sigma env_ar newfs in
     let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in
       if not def && is_impredicative_sort env0 sort then
-        sigma, typ
+        sigma, (univ, typ)
       else
         let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in
         if Univ.is_small_univ univ &&
            Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
 	   (* We can assume that the level in aritysort is not constrained
 	       and clear it, if it is flexible *)
-   Evd.set_eq_sort env_ar sigma Sorts.set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
-        else sigma, typ
+   Evd.set_eq_sort env_ar sigma Sorts.set sort, (univ, EConstr.mkSort (Sorts.sort_of_univ univ))
+        else sigma, (univ, typ)
   in
   let (sigma, typs) = List.fold_left2_map fold sigma typs data in
   let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf ->
       let newps = List.map (RelDecl.map_constr_het nf) newps in
-      let map (impls, newfs) typ =
+      let map (impls, newfs) (univ, typ) =
         let newfs = List.map (RelDecl.map_constr_het nf) newfs in
         let typ = nf typ in
-        (typ, impls, newfs)
+        (univ, typ, impls, newfs)
       in
       let ans = List.map2 map data typs in
       newps, ans)
@@ -295,7 +306,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
   let x = make_annot (Name binder_name) mip.mind_relevance in
   let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
-  let primitive = 
+  let primitive =
     match mib.mind_record with
     | PrimRecord _ -> true
     | FakeRecord | NotRecord -> false
@@ -310,7 +321,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
 	  | Anonymous ->
 	      (None::sp_projs,i,NoProjection fi::subst)
 	  | Name fid -> try
-	    let kn, term = 
+            let kn, term =
 	      if is_local_assum decl && primitive then
                 let p = Projection.Repr.make indsp
                     ~proj_npars:mib.mind_nparams
@@ -345,12 +356,12 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
                   let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
-		      applist (mkConstU (kn,u),proj_args) 
+                      applist (mkConstU (kn,u),proj_args)
                   in
                   Declare.definition_message fid;
 		    kn, constr_fip
                 with Type_errors.TypeError (ctx,te) ->
-                  raise (NotDefinable (BadTypedProj (fid,ctx,te))) 
+                  raise (NotDefinable (BadTypedProj (fid,ctx,te)))
 	    in
             let refi = GlobRef.ConstRef kn in
 	    Impargs.maybe_declare_manual_implicits false refi impls;
@@ -404,29 +415,33 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let binder_name =
     match name with
     | None ->
-      let map (id, _, _, _, _, _, _) =
+      let map (id, _, _, _, _, _, _, _) =
         Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
       in
       Array.map_of_list map record_data
     | Some n -> n
   in
   let ntypes = List.length record_data in
-  let mk_block i (id, idbuild, arity, _, fields, _, _) =
+  let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) =
     let nfields = List.length fields in
     let args = Context.Rel.to_extended_list mkRel nfields params in
     let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
     let type_constructor = it_mkProd_or_LetIn ind fields in
     let template =
+      let template_candidate () =
+        ComInductive.template_polymorphism_candidate (Global.env ()) univs params
+          (Some (Sorts.sort_of_univ min_univ))
+      in
       match template with
       | Some template, _ ->
         (* templateness explicitly requested *)
         if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+        if template && not (template_candidate ()) then
+          user_err Pp.(strbrk "record cannot be made template polymorphic on any universe");
         template
       | None, template ->
         (* auto detect template *)
-        ComInductive.should_auto_template id (template && not poly &&
-        let _, s = Reduction.dest_arity (Global.env()) arity in
-        not (Sorts.is_small s))
+        ComInductive.should_auto_template id (template && template_candidate ())
     in
     { mind_entry_typename = id;
       mind_entry_arity = arity;
@@ -437,7 +452,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let blocks = List.mapi mk_block record_data in
   let primitive =
     !primitive_flag &&
-    List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
+    List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
   in
   let mie =
     { mind_entry_params = params;
@@ -454,7 +469,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
       ~primitive_expected:!primitive_flag
   in
-  let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
+  let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
@@ -469,7 +484,7 @@ let implicits_of_context ctx =
   List.map (fun name -> CAst.make (Some (name,true)))
     (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
-let declare_class def cumulative ubinders univs id idbuild paramimpls params arity
+let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity
     template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -484,7 +499,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
       let binder = {binder with binder_name=Name binder_name} in
       let class_body = it_mkLambda_or_LetIn field params in
       let class_type = it_mkProd_or_LetIn arity params in
-      let class_entry = 
+      let class_entry =
         Declare.definition_entry ~types:class_type ~univs class_body in
       let cst = Declare.declare_constant ~name:id
         (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
@@ -509,18 +524,18 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
       Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
-	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
-	| None -> None 
+        | Some b -> Some ((if b then Backward else Forward), List.hd priorities)
+        | None -> None
       in
       [cref, [Name proj_name, sub, Some proj_cst]]
     | _ ->
-      let record_data = [id, idbuild, arity, fieldimpls, fields, false,
+      let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false,
                          List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
       let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls
         params template ~kind:Decls.Method ~name:[|binder_name|] record_data
       in
-       let coers = List.map2 (fun coe pri -> 
-			      Option.map (fun b -> 
+       let coers = List.map2 (fun coe pri ->
+                              Option.map (fun b ->
 			      if b then Backward, pri else Forward, pri) coe)
 	  coers priorities
        in
@@ -575,7 +590,7 @@ let add_constant_class env sigma cst =
   let ctx, _ = decompose_prod_assum ty in
   let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in
   let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in
-  let tc = 
+  let tc =
     { cl_univs = univs;
       cl_impl = GlobRef.ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
@@ -679,24 +694,24 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records =
   let template = template, auto_template in
   match kind with
   | Class def ->
-    let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
+    let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with
     | [r], [d] -> r, d
     | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
     in
     let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in
     let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in
     declare_class def cumulative ubinders univs id.CAst.v idbuild
-      implpars params arity template implfs fields coers priorities
+      implpars params univ arity template implfs fields coers priorities
   | _ ->
     let map impls = implpars @ [CAst.make None] @ impls in
-    let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
-    let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
+    let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in
+    let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
       let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
           { pf_subclass = not (Option.is_empty rf_subclass);
             pf_canonical = rf_canonical })
           cfs
       in
-      id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
+      id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe
     in
     let data = List.map2 map data records in
     let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4ae9d6d54f..6180ab0821 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -606,6 +606,24 @@ let vernac_assumption ~atts discharge kind l nl =
             | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
   ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
+let set_template_check b =
+ let typing_flags = Environ.typing_flags (Global.env ()) in
+ Global.set_typing_flags { typing_flags with Declarations.check_template = b }
+
+let is_template_check () =
+  let typing_flags = Environ.typing_flags (Global.env ()) in
+  typing_flags.Declarations.check_template
+
+let () =
+  let tccheck =
+    { optdepr = true;
+      optname = "Template universe check";
+      optkey = ["Template"; "Check"];
+      optread = (fun () -> is_template_check ());
+      optwrite = (fun b -> set_template_check b)}
+  in
+    declare_bool_option tccheck
+
 let is_polymorphic_inductive_cumulativity =
   declare_bool_option_and_ref ~depr:false ~value:false
     ~name:"Polymorphic inductive cumulativity"
@@ -2538,7 +2556,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
     VtDefault(fun () ->
         vernac_hints ~atts dbnames hints)
   | VernacSyntacticDefinition (id,c,b) ->
-    VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
+     VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
   | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
     VtDefault(fun () ->
         with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))