#113 closed defect (fixed)
Coq commands not described in coq/coq-syntax.el
| Reported by: | Evgeny Makarov | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | PG-Emacs-3.7 |
| Component: | 2:pg-emacs | Keywords: | Coq vernacular state preserving |
| Cc: |
Description
Hello,
The following commands, given in the "Vernacular Commands Index" in Coq Reference Manual are not listed in coq-commands-db in coq/coq-syntax.el. As a result, they are not highlighted and, more importantly, they are though to be not state preserving and so are not executed by proof-minibuffer-cmd command.
About
Pwd
Search
Test
The "Check" command is mentioned but it is marked as not state preserving as well.
Could you change this?
Thank you, Yevgeniy
Change History (2)
comment:1 Changed 17 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
comment:2 Changed 16 years ago by
| Component: | 1:pg-eclipse → 2:pg-emacs |
|---|
Note: See
TracTickets for help on using
tickets.
Done, thank you for signaling this.
Be aware that Check is available by C-c C-a C-c. Pierre