diff options
| author | Pierre-Marie Pédrot | 2020-04-14 12:24:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-14 12:24:18 +0200 |
| commit | b26d17a6a76b6758d0f22eaa025b1c31b474809f (patch) | |
| tree | f119296a9a545132d81e0a78ade56883968f11d3 /test-suite | |
| parent | 585884b757b8eef4052ddb45b42b15bfce372c0d (diff) | |
| parent | f6f2433eddde8b4e09f2ef72f43db88892d03620 (diff) | |
Merge PR #11985: Fix #11934 equality on constrexpr ignores instances of explicit applications
Ack-by: herbelin
Reviewed-by: ppedrot
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 *) |