diff options
| author | Gaëtan Gilbert | 2020-03-31 16:53:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-06 14:48:17 +0200 |
| commit | f6f2433eddde8b4e09f2ef72f43db88892d03620 (patch) | |
| tree | 0c55e143224098e049f4b3462dc4bf507a639f85 /test-suite | |
| parent | 28c031158cee24faf782a7192032e29229aee4d4 (diff) | |
Fix #11934 equality on constrexpr ignores instances of explicit applications
While we're at it also compare instances in glob_constr although I
don't know if that changes any behaviour.
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 *) |