diff options
| author | Hugo Herbelin | 2020-02-26 19:50:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-26 19:50:21 +0100 |
| commit | f97cb743386744e9da3ede4b6cf8c803c2f58fde (patch) | |
| tree | 587be188c84d33fcdac8cd72c029cfd2be7ac85a /test-suite | |
| parent | 0e70be7868bdc500212631a956b01e94565cd2c3 (diff) | |
| parent | 0dab087b10598f79ffa4f907c6d93fb7932e1c5b (diff) | |
Merge PR #11644: Use implicit arguments in notations for eq.
Reviewed-by: herbelin
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output-coqtop/ShowGoal.out | 6 | ||||
| -rw-r--r-- | test-suite/output-coqtop/ShowGoal.v | 6 | ||||
| -rw-r--r-- | test-suite/output/EqNotation.out | 3 | ||||
| -rw-r--r-- | test-suite/output/EqNotation.v | 2 | ||||
| -rw-r--r-- | test-suite/output/Show.out | 6 |
5 files changed, 14 insertions, 9 deletions
diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out index 2eadd22db8..42d9ff31e9 100644 --- a/test-suite/output-coqtop/ShowGoal.out +++ b/test-suite/output-coqtop/ShowGoal.out @@ -52,19 +52,19 @@ x < 1 subgoal ============================
i = i
-x < goal ID 16 at state 5
+x < goal ID 13 at state 5
i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k
-x < goal ID 16 at state 7
+x < goal ID 13 at state 7
i : nat
============================
i = i /\ i = ?k /\ i = ?k
-x < goal ID 16 at state 9
+x < goal ID 13 at state 9
i : nat
============================
diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v index 9545254770..80996eb169 100644 --- a/test-suite/output-coqtop/ShowGoal.v +++ b/test-suite/output-coqtop/ShowGoal.v @@ -6,6 +6,6 @@ Proof using. trivial. split. trivial. -Show Goal 16 at 5. -Show Goal 16 at 7. -Show Goal 16 at 9. +Show Goal 13 at 5. +Show Goal 13 at 7. +Show Goal 13 at 9. diff --git a/test-suite/output/EqNotation.out b/test-suite/output/EqNotation.out new file mode 100644 index 0000000000..41500a75b9 --- /dev/null +++ b/test-suite/output/EqNotation.out @@ -0,0 +1,3 @@ +The command has indeed failed with message: +Cannot infer the implicit parameter A of eq whose type is +"Type". diff --git a/test-suite/output/EqNotation.v b/test-suite/output/EqNotation.v new file mode 100644 index 0000000000..21076472b8 --- /dev/null +++ b/test-suite/output/EqNotation.v @@ -0,0 +1,2 @@ +(* should mention "the implicit parameter A of eq" *) +Fail Type (forall x, x = x). diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out index ca56f032ff..f02e442be5 100644 --- a/test-suite/output/Show.out +++ b/test-suite/output/Show.out @@ -1,10 +1,10 @@ -3 subgoals (ID 31) +3 subgoals (ID 29) H : 0 = 0 ============================ 1 = 1 -subgoal 2 (ID 35) is: +subgoal 2 (ID 33) is: 1 = S (S m') -subgoal 3 (ID 22) is: +subgoal 3 (ID 20) is: S (S n') = S m |