diff options
| author | Gaëtan Gilbert | 2020-02-20 16:50:24 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-25 13:43:23 +0100 |
| commit | 0dab087b10598f79ffa4f907c6d93fb7932e1c5b (patch) | |
| tree | 7a49e711046ea7ef5071f448da669c546c5409c9 /test-suite/output-coqtop | |
| parent | 1bc8cd6390a3208659d563b1363f9bc0d87643a0 (diff) | |
Use implicit arguments in notations for eq.
This gives IMO slightly nicer errors when the type cannot be inferred,
ie
~~~coq
Type (forall x, x = x).
~~~
says "cannot infer the implicit parameter A of eq" instead of "cannot
infer this placeholder".
Diffstat (limited to 'test-suite/output-coqtop')
| -rw-r--r-- | test-suite/output-coqtop/ShowGoal.out | 6 | ||||
| -rw-r--r-- | test-suite/output-coqtop/ShowGoal.v | 6 |
2 files changed, 6 insertions, 6 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. |