Merge PR #8488: Warning when using automatic template polymorphism

5 files changed, 8 insertions, 0 deletions

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.