diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Template.v | 16 |
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] |