Merge PR #8488: Warning when using automatic template polymorphism

12 files changed, 16 insertions, 14 deletions

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.