Opened 10 years ago
Closed 9 years ago
#494 closed defect (fixed)
PG incorrectly parses the result of [Fail] in some cases
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | coq coq-trunk Fail Ltac |
| Cc: | jasongross9+pg@… |
Description
In, e.g., the code
Ltac f := fail. Goal True. Fail f.
coqtop -emacs returns
The command has indeed failed with message: => In nested Ltac calls to "f", last call failed. Error: Tactic failure.
which PG assumes means that there was an error.
In other cases, PG sees "=> Error", which it takes to mean is not an error.
Change History (2)
comment:1 Changed 9 years ago by
comment:2 Changed 9 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
It seems fixed in recent v8.4 and v8.5, the message is now enclosed into <infomsg> which prevents it as being seen as an error message.
Note: See
TracTickets for help on using
tickets.
Not sure how relevant this is to 8.5, since Fail does not include the Error header anymore. -- cpitcla