From 3881fb7b93196a304b332ae81f1debde1ce9aaf9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 23 Aug 2018 11:32:52 +0200
Subject: Add explicit atribute for template polymorphism.

---
 test-suite/success/Template.v | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 test-suite/success/Template.v

(limited to 'test-suite')

diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
new file mode 100644
index 0000000000..a8fe1baa1b
--- /dev/null
+++ b/test-suite/success/Template.v
@@ -0,0 +1,36 @@
+Set Printing Universes.
+
+Module Auto.
+  Inductive Box (A:Type) : Type := box : A -> Box A.
+
+  About Box.
+
+  (* This checks that Box is template poly, see module No for how it fails *)
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Definition box_lti A := Box A : Type@{i}.
+
+End Auto.
+
+Module Yes.
+  #[template]
+  Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A.
+
+  About Box.
+
+  Universe i j. Constraint i < j.
+  Definition j_lebox (A:Type@{j}) := Box A.
+  Definition box_lti A := Box A : Type@{i}.
+
+End Yes.
+
+Module No.
+  #[notemplate]
+  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 No.
-- 
cgit v1.2.3


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