diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-20 01:34:36 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-20 01:34:36 +0200 |
| commit | b7cf93cec115b61889e31c0abefdbd29d9b51ebe (patch) | |
| tree | 8cc84e9c2ae8de301e10d8ea3f2d12303dfb126b /test-suite | |
| parent | 7dc84057e3596b1c3f6ec869daebcfa8747f5c12 (diff) | |
| parent | 741f3fab052b91eaec57f32b639ca722c3d8dc34 (diff) | |
Merge PR#474: A fix for #5390 (a useful error on used introduction names was masked).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Tactics.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Tactics.v | 10 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 239edd1da..19c9fc442 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -2,3 +2,7 @@ Ltac f H := split; [ a H | e H ] Ltac g := match goal with | |- context [ if ?X then _ else _ ] => case X end +The command has indeed failed with message: +H is already used. +The command has indeed failed with message: +H is already used. diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index a7c497cfa..9a5edb813 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -11,3 +11,13 @@ Print Ltac f. Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end. Print Ltac g. + +(* Test an error message (#5390) *) +Lemma myid (P : Prop) : P <-> P. +Proof. split; auto. Qed. + +Goal True -> (True /\ True) -> True. +Proof. +intros H. +Fail intros [H%myid ?]. +Fail destruct 1 as [H%myid ?]. |