diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-11-28 19:05:23 +0100 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-12-02 16:47:45 +0100 |
commit | af58f731322527af1d81233beade4c98fbb2d7bd (patch) | |
tree | 81e811e0c16f37c8c920714bbca57c91dfb84b0d /test-suite/bugs/closed | |
parent | a27ac0315dcbb99c64a260bac3988199a26b39cf (diff) |
Univs: fix bug #5188
Parameter was implemented the wrong way trying to separate the universes
of the telescope.
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/5188.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5188.v b/test-suite/bugs/closed/5188.v new file mode 100644 index 000000000..e29ebfb4e --- /dev/null +++ b/test-suite/bugs/closed/5188.v @@ -0,0 +1,5 @@ +Set Printing All. +Axiom relation : forall (T : Type), Set. +Axiom T : forall A (R : relation A), Set. +Set Printing Universes. +Parameter (A:_) (R:_) (e:@T A R). |