Merge PR #8488: Warning when using automatic template polymorphism

28 files changed, 47 insertions, 0 deletions

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