1 files changed, 36 insertions, 0 deletions
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.