Merge PR #8303: Better controls for template polymorphism

1 files changed, 48 insertions, 0 deletions

diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
new file mode 100644
index 0000000000..1c6e2d81d8
--- /dev/null
+++ b/test-suite/success/Template.v
@@ -0,0 +1,48 @@
+Set Printing Universes.
+
+Module AutoYes.
+  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 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]
+  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.