Merge PR #8488: Warning when using automatic template polymorphism

14 files changed, 38 insertions, 1 deletions

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.