Add option to control automatic template polymorphism.

1 files changed, 14 insertions, 2 deletions

diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index a8fe1baa1b..1c6e2d81d8 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -1,6 +1,6 @@
 Set Printing Universes.
 
-Module Auto.
+Module AutoYes.
   Inductive Box (A:Type) : Type := box : A -> Box A.
 
   About Box.
@@ -10,7 +10,19 @@ Module Auto.
   Definition j_lebox (A:Type@{j}) := Box A.
   Definition box_lti A := Box A : Type@{i}.
 
-End Auto.
+End AutoYes.
+
+Module AutoNo.
+  Unset Auto Template Polymorphism.
+  Inductive Box (A:Type) : Type := box : A -> Box A.
+
+  About Box.
+
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Fail Definition box_lti A := Box A : Type@{i}.
+
+End AutoNo.
 
 Module Yes.
   #[template]