Custom Query (361 matches)
Results (58 - 60 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #113 | fixed | Coq commands not described in coq/coq-syntax.el | ||
| 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 |
|||
| #331 | fixed | Coq config for proof-goal-command and proof-save-command | ||
| Description |
The convenient functions I would suggest to remove the unnecessary last-but-one spaces: "Goal %s. " and "Save %s. " will be closer to Coq standard phrasing. Kind regards, Erik. |
|||
| #233 | fixed | Coq fails to start | ||
| Description |
OS: Mac OS X 10.5.4 PG version: 3.7.1 Gnu Emacs version: 22.2.1 (via MacPorts?), 23.0.60.1 (via CVS) Coq version: 8.1pl3 Test file: A single line consisting of "Definition x : nat := 3." Problem: Coq fails to start when I try to process the line or buffer. The only error message that I see is "Wrong type argument: integerp, "-emacs-U"." (For the CVS version of emacs, it's characterp instead of integerp.) In the *Messages* buffer, I see "let*: Wrong type argument: integerp, "-emacs-U" [2 times]." I don't think I'm seeing this problem with PG 3.7. My contact: brian.aydemir [ at ] gmail.com Cheers, Brian Aydemir |
|||
