Merge PR #8488: Warning when using automatic template polymorphism

58 files changed, 131 insertions, 21 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 7122b48809..6789bc038e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -135,6 +135,17 @@ Universes
   for the "Private Polymorphic Universes" option (and Unset it to get
   the previous behaviour).
 
+Inductives
+
+- An option and attributes to control the automatic decision to
+  declare an inductive type as template polymorphic were added.
+  Warning "auto-template" will trigger when an inductive is
+  automatically declared template polymorphic without the attribute.
+
+Funind
+
+- Inductive types declared by Funind will never be template polymorphic.
+
 Misc
 
 - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances.
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 98aaa081c3..4b6caea70d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1494,7 +1494,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 4042959b50..eb84b1203d 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -118,6 +118,7 @@ Section MakeRingPol.
     - (Pinj i (Pc c)) is (Pc c)
  *)
 
+ #[universes(template)]
  Inductive Pol : Type :=
   | Pc : C -> Pol
   | Pinj : positive -> Pol -> Pol
@@ -939,6 +940,7 @@ Qed.
 
  (** Definition of polynomial expressions *)
 
+ #[universes(template)]
  Inductive PExpr : Type :=
   | PEc : C -> PExpr
   | PEX : positive -> PExpr
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index f066ea462f..782fab5e68 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -289,6 +289,7 @@ destruct o' ; rewrite H1 ; now rewrite  (Rplus_0_l sor).
  now apply (Rplus_nonneg_nonneg sor).
 Qed.
 
+#[universes(template)]
 Inductive Psatz : Type :=
 | PsatzIn : nat -> Psatz
 | PsatzSquare : PolC -> Psatz
@@ -685,6 +686,7 @@ end.
 Definition  eval_pexpr : PolEnv -> PExpr C -> R :=
  PEeval rplus rtimes rminus ropp phi pow_phi rpow.
 
+#[universes(template)]
 Record Formula (T:Type) : Type := {
   Flhs : PExpr T;
   Fop : Op2;
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 458844e1b9..587f2f1fa4 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -21,6 +21,7 @@ Require Import Bool.
 Set Implicit Arguments.
 
 
+  #[universes(template)]
   Inductive BFormula (A:Type) : Type :=
   | TT   : BFormula A
   | FF   : BFormula A
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 2d2c0bc77a..c888f9af45 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -30,6 +30,7 @@ Section MakeVarMap.
   Variable A : Type.
   Variable default : A.
 
+  #[universes(template)]
   Inductive t  : Type :=
   | Empty : t
   | Leaf : A -> t
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 99c02995fb..751f0d8334 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -81,10 +81,12 @@ Section Store.
 
 Variable A:Type.
 
+#[universes(template)]
 Inductive Poption : Type:=
   PSome : A -> Poption
 | PNone : Poption.
 
+#[universes(template)]
 Inductive Tree : Type :=
    Tempty : Tree
  | Branch0 : Tree -> Tree -> Tree
@@ -177,6 +179,7 @@ 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}.
 
@@ -191,6 +194,7 @@ 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 ce115f564f..dba72337b2 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -730,6 +730,7 @@ Qed.
 
 (* The input: syntax of a field expression *)
 
+#[universes(template)]
 Inductive FExpr : Type :=
  | FEO : FExpr
  | FEI : FExpr
@@ -762,6 +763,7 @@ Strategy expand [FEeval].
 
 (* The result of the normalisation *)
 
+#[universes(template)]
 Record linear : Type := mk_linear {
    num : PExpr C;
    denum : PExpr C;
@@ -944,6 +946,7 @@ 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 f5db275465..15d490a6ab 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -740,6 +740,7 @@ 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 12208ff6b9..31182f51e2 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -32,6 +32,7 @@ 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. 
@@ -43,6 +44,7 @@ Definition cI:C . exact ring1. Defined.
  Definition P1 := Pc 1.
 
 Variable Ceqb:C->C->bool.
+#[universes(template)]
 Class Equalityb (A : Type):= {equalityb : A -> A -> bool}.
 Notation "x =? y" := (equalityb x y) (at level 70, no associativity).
 Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y).
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index ccd82eabcd..9ef24144d2 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -121,6 +121,7 @@ Section MakeRingPol.
     - (Pinj i (Pc c)) is (Pc c)
  *)
 
+ #[universes(template)]
  Inductive Pol : Type :=
   | Pc : C -> Pol
   | Pinj : positive -> Pol -> Pol
@@ -908,6 +909,7 @@ 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 d67a8d8dce..6c782269ab 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -540,6 +540,7 @@ 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/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 3a7cf41d43..ed4ff2aa66 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -609,6 +609,7 @@ Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
 (**  Allow the direct application of a reflection lemma to a boolean assertion.  **)
 Coercion elimT : reflect >-> Funclass.
 
+#[universes(template)]
 Variant implies P Q := Implies of P -> Q.
 Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed.
 Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P.
@@ -1130,10 +1131,12 @@ Proof. by move=> *; apply/orP; left. Qed.
 Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).
 Proof. by move=> *; apply/orP; right. Qed.
 
+#[universes(template)]
 Variant mem_pred := Mem of pred T.
 
 Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]).
 
+#[universes(template)]
 Structure predType := PredType {
   pred_sort :> Type;
   topred : pred_sort -> pred T;
@@ -1275,6 +1278,7 @@ Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT).
  implementation of unification, notably improper expansion of telescope
  projections and overwriting of a variable assignment by a later
  unification (probably due to conversion cache cross-talk).                  **)
+#[universes(template)]
 Structure manifest_applicative_pred p := ManifestApplicativePred {
   manifest_applicative_pred_value :> pred T;
   _ : manifest_applicative_pred_value = p
@@ -1283,18 +1287,21 @@ Definition ApplicativePred p := ManifestApplicativePred (erefl p).
 Canonical applicative_pred_applicative sp :=
   ApplicativePred (applicative_pred_of_simpl sp).
 
+#[universes(template)]
 Structure manifest_simpl_pred p := ManifestSimplPred {
   manifest_simpl_pred_value :> simpl_pred T;
   _ : manifest_simpl_pred_value = SimplPred p
 }.
 Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)).
 
+#[universes(template)]
 Structure manifest_mem_pred p := ManifestMemPred {
   manifest_mem_pred_value :> mem_pred T;
   _ : manifest_mem_pred_value= Mem [eta p]
 }.
 Canonical expose_mem_pred p :=  @ManifestMemPred p _ (erefl _).
 
+#[universes(template)]
 Structure applicative_mem_pred p :=
   ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}.
 Canonical check_applicative_mem_pred p (ap : manifest_applicative_pred p) mp :=
@@ -1345,6 +1352,7 @@ End simpl_mem.
 
 (**  Qualifiers and keyed predicates.  **)
 
+#[universes(template)]
 Variant qualifier (q : nat) T := Qualifier of predPredType T.
 
 Coercion has_quality n T (q : qualifier n T) : pred_class :=
@@ -1392,9 +1400,11 @@ Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B))
 Section KeyPred.
 
 Variable T : Type.
+#[universes(template)]
 Variant pred_key (p : predPredType T) := DefaultPredKey.
 
 Variable p : predPredType T.
+#[universes(template)]
 Structure keyed_pred (k : pred_key p) :=
   PackKeyedPred {unkey_pred :> pred_class; _ : unkey_pred =i p}.
 
@@ -1426,6 +1436,7 @@ 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 7596f6638a..4721e19a8b 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -178,6 +178,7 @@ 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.
 
 (**
@@ -206,6 +207,7 @@ Inductive external_view : Type := tactic_view of Type.
 
 Module TheCanonical.
 
+#[universes(template)]
 Variant put vT sT (v1 v2 : vT) (s : sT) := Put.
 
 Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
@@ -301,9 +303,11 @@ Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
    We also define a simpler version ("phant" / "Phant") of phantom for the
  common case where p_type is Type.                                           **)
 
+#[universes(template)]
 Variant phantom T (p : T) := Phantom.
 Arguments phantom : clear implicits.
 Arguments Phantom : clear implicits.
+#[universes(template)]
 Variant phant (p : Type) := Phant.
 
 (**  Internal tagging used by the implementation of the ssreflect elim.  **)
@@ -389,6 +393,7 @@ Ltac ssrdone0 :=
    | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
 
 (**  To unlock opaque constants.  **)
+#[universes(template)]
 Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}.
 Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed.
 
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 6535cad8b7..b51ffada0c 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -285,6 +285,7 @@ Lemma unitE : all_equal_to tt. Proof. by case. Qed.
 
 (**  A generic wrapper type  **)
 
+#[universes(template)]
 Structure wrapped T := Wrap {unwrap : T}.
 Canonical wrap T x := @Wrap T x.
 
@@ -334,6 +335,7 @@ Section SimplFun.
 
 Variables aT rT : Type.
 
+#[universes(template)]
 Variant simpl_fun := SimplFun of aT -> rT.
 
 Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 43718a0f07..4e949dcb04 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -43,6 +43,7 @@ Print foo.
 
 (* Accept and use notation with binded parameters *)
 
+#[universes(template)]
 Inductive I (A: Type) : Type := C : A -> I A.
 Notation "x <: T" := (C T x) (at level 38).
 
@@ -83,6 +84,7 @@ 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 0e84bf3966..6976f35a88 100644
--- a/test-suite/output/Coercions.v
+++ b/test-suite/output/Coercions.v
@@ -1,7 +1,7 @@
 (* Submitted by Randy Pollack *)
 
-Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
-Record rel (S : Set) : Type :=  {sr_rel :> S -> S -> Prop}.
+#[universes(template)] Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
+#[universes(template)] 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 1ecd9771eb..f9398fdca9 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.
 
- Inductive decoder_result : Type :=
+ #[universes(template)] 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 61ae4edbd1..9b25c2dbd3 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.
 
-CoInductive Inf := S { projS : Inf }.
+#[universes(template)] 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/Inductive.v b/test-suite/output/Inductive.v
index 8ff91268a6..9eec9a7dad 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -3,5 +3,5 @@ Fail Inductive list' (A:Set) : Set :=
 | cons' : A -> list' A -> list' (A*A).
 
 (* Check printing of let-ins *)
-Inductive foo (A : Type) (x : A) (y := x) := Foo.
+#[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo.
 Print foo.
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 15211f1233..2caffad1d9 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                                             *)
 
-Inductive ftele : Type :=
+#[universes(template)] 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 d671053c07..0c1b08f5a3 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. *)
 
-Inductive Fin (n:nat) := Z : Fin n.
+#[universes(template)] 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/Projections.v b/test-suite/output/Projections.v
index 098a518dc4..2713e6a188 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -5,7 +5,7 @@ Class HostFunction := host_func : Type.
 
 Section store.
   Context `{HostFunction}.
-  Record store := { store_funcs : host_func }.
+  #[universes(template)] 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 d9a649fadc..4fe7b051f8 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.
 
-Record N := C { T : Type; _ : True }.
+#[universes(template)] 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).
 
-Record M := D { U : Type; a := 0; q : True }.
+#[universes(template)] 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 9cf6ad35b8..99183f2064 100644
--- a/test-suite/output/ShowMatch.v
+++ b/test-suite/output/ShowMatch.v
@@ -3,12 +3,12 @@
 *)
 
 Module A.
-  Inductive foo := f.
+  #[universes(template)] Inductive foo := f.
   Show Match foo. (* no need to disambiguate *)
 End A. 
 
 Module B.
-  Inductive foo := f.
+  #[universes(template)] 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/Warnings.v b/test-suite/output/Warnings.v
index 7465442cab..0eb5db1733 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 *)
-Record A := { B:Type; b:B->B }.
+#[universes(template)] 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 57a4739e9f..209fedc343 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... *)
 
-Inductive T (n:nat) : Type := A : T n.
+#[universes(template)] 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/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 86a3a88be9..4b97d75cea 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -283,6 +283,7 @@ 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 2673a11917..e6968bd6c2 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -27,6 +27,7 @@ Require Export Coq.Classes.Morphisms.
 
 (** A setoid wraps an equivalence. *)
 
+#[universes(template)]
 Class Setoid A := {
   equiv : relation A ;
   setoid_equiv :> Equivalence equiv }.
@@ -128,6 +129,7 @@ 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/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 8fc04d81e6..9a815d2a7e 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -53,6 +53,7 @@ Variable elt : Type.
 
    The fifth field of [Node] is the height of the tree *)
 
+#[universes(template)]
 Inductive tree :=
   | Leaf : tree
   | Node : tree -> key -> elt -> tree -> int -> tree.
@@ -235,6 +236,7 @@ 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).
 
@@ -291,6 +293,7 @@ Variable cmp : elt->elt->bool.
 
 (** ** Enumeration of the elements of a tree *)
 
+#[universes(template)]
 Inductive enumeration :=
  | End : enumeration
  | More : key -> elt -> t -> enumeration -> enumeration.
@@ -1817,6 +1820,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Module Raw := Raw I X.
  Import Raw.Proofs.
 
+ #[universes(template)]
  Record bst (elt:Type) :=
   Bst {this :> Raw.tree elt; is_bst : Raw.bst this}.
 
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 950b30ee4d..7bc9edff8d 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -451,6 +451,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Import Raw.
  Import Raw.Proofs.
 
+ #[universes(template)]
  Record bbst (elt:Type) :=
   Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}.
 
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 6ca158a277..4febd64842 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -1024,6 +1024,7 @@ 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/FMapPositive.v b/theories/FSets/FMapPositive.v
index 0fc68b1433..b47c99244b 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -73,6 +73,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Definition key := positive : Type. 
 
+  #[universes(template)]
   Inductive tree (A : Type) :=
     | Leaf : tree A
     | Node : tree A -> option A -> tree A -> tree A.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 03dce9666d..a923f4e6f9 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -869,6 +869,7 @@ 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 7f0387dd12..3603604a71 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -167,6 +167,7 @@ Register S as num.nat.S.
 
 (** [option A] is the extension of [A] with an extra element [None] *)
 
+#[universes(template)]
 Inductive option (A:Type) : Type :=
   | Some : A -> option A
   | None : option A.
@@ -186,6 +187,7 @@ Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
 
 (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
 
+#[universes(template)]
 Inductive sum (A B:Type) : Type :=
   | inl : A -> sum A B
   | inr : B -> sum A B.
@@ -198,6 +200,7 @@ Arguments inr {A B} _ , A [B] _.
 (** [prod A B], written [A * B], is the product of [A] and [B];
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
 
+#[universes(template)]
 Inductive prod (A B:Type) : Type :=
   pair : A -> B -> A * B
 
@@ -256,6 +259,7 @@ Defined.
 
 (** Polymorphic lists and some operations *)
 
+#[universes(template)]
 Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.
@@ -384,6 +388,7 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined.
     member is the singleton datatype [identity A a a] whose
     sole inhabitant is denoted [identity_refl A a] *)
 
+#[universes(template)]
 Inductive identity (A:Type) (a:A) : A -> Type :=
   identity_refl : identity a a.
 Hint Resolve identity_refl: core.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index e4796a8059..cfba2bae69 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -24,6 +24,7 @@ Require Import Logic.
     Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset
     of elements of the type [A] which satisfy both [P] and [Q]. *)
 
+#[universes(template)]
 Inductive sig (A:Type) (P:A -> Prop) : Type :=
     exist : forall x:A, P x -> sig P.
 
@@ -31,12 +32,14 @@ Register sig as core.sig.type.
 Register exist as core.sig.intro.
 Register sig_rect as core.sig.rect.
 
+#[universes(template)]
 Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
     exist2 : forall x:A, P x -> Q x -> sig2 P Q.
 
 (** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type.
     Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
 
+#[universes(template)]
 Inductive sigT (A:Type) (P:A -> Type) : Type :=
     existT : forall x:A, P x -> sigT P.
 
@@ -44,6 +47,7 @@ Register sigT as core.sigT.type.
 Register existT as core.sigT.intro.
 Register sigT_rect as core.sigT.rect.
 
+#[universes(template)]
 Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
     existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
 
@@ -700,6 +704,7 @@ Register sumbool as core.sumbool.type.
 (** [sumor] is an option type equipped with the justification of why
     it may not be a regular value *)
 
+#[universes(template)]
 Inductive sumor (A:Type) (B:Prop) : Type :=
   | inleft : A -> A + {B}
   | inright : B -> A + {B}
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index 57f558de50..d93816e9ff 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -78,6 +78,7 @@ 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.
 
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 8a01b8fb19..a03799959e 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -16,6 +16,7 @@ Section Streams.
 
 Variable A : Type.
 
+#[universes(template)]
 CoInductive Stream : Type :=
     Cons : A -> Stream -> Stream.
 
diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v
index 02c8998a8d..a70bd92329 100644
--- a/theories/Logic/ExtensionalityFacts.v
+++ b/theories/Logic/ExtensionalityFacts.v
@@ -40,6 +40,7 @@ Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g
 
 (** The diagonal over A and the one-one correspondence with A *)
 
+#[universes(template)]
 Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }.
 
 Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index ac2a143472..13e1dad361 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -208,6 +208,7 @@ 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 888f9850c1..a3dcca7dfd 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -48,6 +48,7 @@ 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.
@@ -167,6 +168,7 @@ end.
 (** Enumeration of the elements of a tree. This corresponds
     to the "samefringe" notion in the litterature. *)
 
+#[universes(template)]
 Inductive enumeration :=
  | End : enumeration
  | More : elt -> tree -> enumeration -> enumeration.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index a4bbaef52d..0ba2799bfb 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -439,6 +439,7 @@ 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/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 951a4ef2b0..9f718cba65 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -28,6 +28,7 @@ Local Open Scope Z_scope.
 
 Module ZnZ.
 
+ #[universes(template)]
  Class Ops (t:Type) := MkOps {
 
     (* Conversion functions with Z *)
diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v
index fe0476e4de..b6441bb76a 100644
--- a/theories/Numbers/Cyclic/Abstract/DoubleType.v
+++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v
@@ -22,6 +22,7 @@ Section Carry.
 
  Variable A : Type.
 
+ #[universes(template)]
  Inductive carry :=
   | C0 : A -> carry
   | C1 : A -> carry.
@@ -44,6 +45,7 @@ Section Zn2Z.
      first.
  *)
 
+ #[universes(template)]
  Inductive zn2z :=
   | W0 : zn2z
   | WW : znz -> znz -> zn2z.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index cf42ed18db..5ae933d433 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -257,6 +257,7 @@ Ltac blocked t := block_goal ; t ; unblock_goal.
    be used by the [equations] resolver. It is especially useful to register the dependent elimination
    principles for things in [Prop] which are not automatically generated. *)
 
+#[universes(template)]
 Class DependentEliminationPackage (A : Type) :=
   { elim_type : Type ; elim : elim_type }.
 
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index ceac021ef2..49a485c741 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -137,6 +137,7 @@ 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 e3e995d201..b6b72de889 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -116,6 +116,7 @@ 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 171dba5522..f94b5cab65 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -380,6 +380,7 @@ 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 61fe55770b..2ed422ffe9 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -100,9 +100,11 @@ 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 a79ddead20..6a8a3014c3 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -22,6 +22,7 @@ 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 17fc0ed25e..5b51c7b953 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -36,6 +36,7 @@ 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 6a22501afa..f5cda792ce 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -42,6 +42,7 @@ Section defs.
   Let emptyBag := EmptyBag A.
   Let singletonBag := SingletonBag _ eqA_dec.
 
+  #[universes(template)]
   Inductive Tree :=
     | Tree_Leaf : Tree
     | Tree_Node : A -> Tree -> Tree -> Tree.
@@ -128,6 +129,7 @@ Section defs.
 
   (** ** Merging two sorted lists *)
 
+  #[universes(template)]
   Inductive merge_lem (l1 l2:list A) : Type :=
     merge_exist :
     forall l:list A,
@@ -201,6 +203,7 @@ Section defs.
 
   (** ** Specification of heap insertion *)
 
+  #[universes(template)]
   Inductive insert_spec (a:A) (T:Tree) : Type :=
     insert_exist :
     forall T1:Tree,
@@ -234,6 +237,7 @@ Section defs.
 
   (** ** Building a heap from a list *)
 
+  #[universes(template)]
   Inductive build_heap (l:list A) : Type :=
     heap_exist :
     forall T:Tree,
@@ -258,6 +262,7 @@ Section defs.
 
   (** ** Building the sorted list *)
 
+  #[universes(template)]
   Inductive flat_spec (T:Tree) : Type :=
     flat_exist :
     forall l:list A,
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 7f96aa6b87..906cf79ca9 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -28,6 +28,7 @@ Local Open Scope nat_scope.
 (**
 A vector is a list of size n whose elements belong to a set A. *)
 
+#[universes(template)]
 Inductive t A : nat -> Type :=
   |nil : t A 0
   |cons : forall (h:A) (n:nat), t A n -> t A (S n).
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index fd363d02ca..cf46657d36 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -18,6 +18,7 @@ Section WellOrdering.
   Variable A : Type.
   Variable B : A -> Type.
 
+  #[universes(template)]
   Inductive WO : Type :=
     sup : forall (a:A) (f:B a -> WO), WO.
 
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 1e35370d29..0b0ed48d51 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -212,6 +212,7 @@ 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/vernac/comInductive.ml b/vernac/comInductive.ml
index 4af6415a4d..348e76da62 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -34,6 +34,13 @@ module RelDecl = Context.Rel.Declaration
 
 (* 3b| Mutual inductive definitions *)
 
+let warn_auto_template =
+  CWarnings.create ~name:"auto-template" ~category:"vernacular"
+    (fun id ->
+       Pp.(strbrk "Automatically declaring " ++ Id.print id ++
+           strbrk " as template polymorphic. Use attributes or " ++
+           strbrk "disable Auto Template Polymorphism to avoid this warning."))
+
 let should_auto_template =
   let open Goptions in
   let auto = ref true in
@@ -44,7 +51,10 @@ let should_auto_template =
         optread  = (fun () -> !auto);
         optwrite = (fun b -> auto := b); }
   in
-  fun () -> !auto
+  fun id would_auto ->
+    let b = !auto && would_auto in
+    if b then warn_auto_template id;
+    b
 
 let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
   | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
@@ -431,8 +441,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
           if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
           template
         | None ->
-          should_auto_template () && not poly &&
-          Option.cata (fun s -> not (Sorts.is_small s)) false concl
+          should_auto_template ind.ind_name (not poly &&
+          Option.cata (fun s -> not (Sorts.is_small s)) false concl)
       in
       { mind_entry_typename = ind.ind_name;
         mind_entry_arity = arity;
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 9df8f7c341..1d6f652385 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -46,7 +46,10 @@ val declare_mutual_inductive_with_eliminations :
   mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
   MutInd.t
 
-val should_auto_template : unit -> bool
+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. *)
 
 (** Exported for Funind *)
 
diff --git a/vernac/record.ml b/vernac/record.ml
index ffd4f654c6..2867ad1437 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -415,9 +415,9 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
         template
       | None, template ->
         (* auto detect template *)
-        ComInductive.should_auto_template () && template && not poly &&
+        ComInductive.should_auto_template id (template && not poly &&
         let _, s = Reduction.dest_arity (Global.env()) arity in
-        not (Sorts.is_small s)
+        not (Sorts.is_small s))
     in
     { mind_entry_typename = id;
       mind_entry_arity = arity;