diff options
| author | Maxime Dénès | 2016-09-30 12:51:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-30 12:51:16 +0200 |
| commit | 7543449792d417a92092b692986d62b622b78ffc (patch) | |
| tree | 8244b6c3efa88abe12ab990a4ae4b3d0af8f5dc1 /test-suite | |
| parent | bff880ffb6ef33c99a96e7925c995b31b1497e6a (diff) | |
| parent | 9615c025a2a09b69f2001d44a66a1fddef74e680 (diff) | |
Merge remote-tracking branch 'github/pr/299' into v8.6
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4869.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v new file mode 100644 index 0000000000..6d21b66fe9 --- /dev/null +++ b/test-suite/bugs/closed/4869.v @@ -0,0 +1,18 @@ +Universes i. + +Fail Constraint i < Set. +Fail Constraint i <= Set. +Fail Constraint i = Set. +Constraint Set <= i. +Constraint Set < i. +Fail Constraint i < j. (* undeclared j *) +Fail Constraint i < Type. (* anonymous *) + +Set Universe Polymorphism. + +Section Foo. + Universe j. + Constraint Set < j. + + Definition foo := Type@{j}. +End Foo.
\ No newline at end of file |