aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Existentials.out
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-02 11:54:25 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-02 16:17:30 +0200
commit351adedc4d154f9f60a3a01b2e906ce2063e323f (patch)
treec5c008f42a03a9bfc5dbf074f4e16395c1037e5a /test-suite/output/Existentials.out
parent93de73a77ffe64fef2f203fc638969466506e417 (diff)
An evar name changed in output test.
Diffstat (limited to 'test-suite/output/Existentials.out')
-rw-r--r--test-suite/output/Existentials.out2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 52e1e0ed0..9d056c4ae 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -2,4 +2,4 @@ Existential 1 =
?Goal1 : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
Existential 2 =
?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used)
-Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y]
+Existential 3 = ?Goal : [q : nat n : nat m : nat |- n = ?y]