diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/bug_11934.out | 13 | ||||
| -rw-r--r-- | test-suite/output/bug_11934.v | 13 |
2 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/output/bug_11934.out b/test-suite/output/bug_11934.out new file mode 100644 index 0000000000..072136c82e --- /dev/null +++ b/test-suite/output/bug_11934.out @@ -0,0 +1,13 @@ +thing = forall x y : foo, bla x y + : Prop +thing = +forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y + : Prop +(* {thing.u1 thing.u0} |= bla.u0 = thing.u0 + bla.u1 = thing.u1 *) +thing = +forall (x : @foo@{thing.u0} True) (y : @foo@{thing.u1} True), +@bla True True x y + : Prop +(* {thing.u1 thing.u0} |= bla.u0 = thing.u0 + bla.u1 = thing.u1 *) diff --git a/test-suite/output/bug_11934.v b/test-suite/output/bug_11934.v new file mode 100644 index 0000000000..fe9772dc62 --- /dev/null +++ b/test-suite/output/bug_11934.v @@ -0,0 +1,13 @@ +Polymorphic Axiom foo@{u} : Prop -> Prop. +Arguments foo {_}. + +Axiom bla : forall {A B}, @foo A -> @foo B -> Prop. +Definition thing := forall (x:@foo@{Type} True) (y:@foo@{Type} True), bla x y. + +Print thing. (* forall x y : foo, bla x y *) + +Set Printing Universes. +Print thing. (* forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y *) + +Set Printing Implicit. +Print thing. (* BAD: forall x y : @foo@{thing.u0} True, @bla True True x y *) |