diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Existentials.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Extraction_matchs_2413.out | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index 483a9ea7..52e1e0ed 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,5 +1,5 @@ Existential 1 = -?Goal0 : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +?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 = ?e : [q : nat n : nat m : nat |- n = ?y] +Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out index 848abd00..f738b0d0 100644 --- a/test-suite/output/Extraction_matchs_2413.out +++ b/test-suite/output/Extraction_matchs_2413.out @@ -4,7 +4,7 @@ let test1 b = b (** val test2 : bool -> bool **) -let test2 b = +let test2 _ = False (** val wrong_id : 'a1 hole -> 'a2 hole **) |