From 6ccacec1b70b9de0ddd8d098f25c367ed975120a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 Aug 2018 11:38:36 +0200
Subject: Add option to control automatic template polymorphism.

---
 test-suite/success/Template.v | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'test-suite')

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]
-- 
cgit v1.2.3