diff options
| author |  Jason Gross <jgross@mit.edu> | 2014-04-08 01:42:49 -0400 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-10 15:39:30 +0200 |
| commit | 3f64bd23a343bcd7be0ef07afa7d9e3249df24ec (patch) | |
| tree | b3a938d606daa421a6e8d566d69fdc93b99f88fd /test-suite/bugs/closed/HoTT_coq_113.v | |
| parent | 3507f3d81082f5f4aef165cc3f4b0207224fb0cb (diff) | |
Add more regression tests for univ poly/prim proj
hese regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.
These are the tests that trunk currently fails.
I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_113.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_113.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_113.v b/test-suite/bugs/closed/HoTT_coq_113.v new file mode 100644 index 000000000..3ef531bc9 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_113.v @@ -0,0 +1,19 @@ +(* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from 55 lines to 38 lines, then from 46 lines to 16 lines *) + +Generalizable All Variables. +Set Universe Polymorphism. +Class Foo (A : Type) := {}. +Definition Baz := Foo. +Definition Bar {A B} `{Foo A, Foo B} : True. +Proof. + Set Printing Universes. + (* [change] should give fresh universes for each [Foo] *) + change Foo with Baz in *. + admit. +Defined. +Definition foo := @Bar nat. +Check @foo Set. +(* Toplevel input, characters 26-29: +Error: +The term "Set" has type "Type (* Set+1 *)" while it is expected to have type + "Set" (Universe inconsistency: Cannot enforce Set < Set because Set = Set)). *) |