Custom Query (361 matches)
Results (37 - 39 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 |
|||
| #114 | fixed | Spurious "replaced xyz occurrences" messages | ||
| Description |
I keep getting "Replaced xyz occurrences" in the xemacs minibuffer after each PG interaction, where xyz depends on the length of the text. As Makarius said, we don't think it is a PG but an xemacs thing. But since you asked me to put it here... Clemens seems to be using the same setup but gets no such message. I started getting it after updating my MAC OS and my xemacs to [version 21.4.20; April 2007]. Tobias |
|||
| #115 | fixed | Isabelle find-theorems form | ||
| Description |
Contribution from Tjark Weber: We have a tested and (hopefully) stable version of the search form now, that I think is ready to be integrated with the CVS version of ProofGeneral. I don't have write access to the CVS repository, so I'm sending the files to you instead. The attached archive contains two files: ProofGeneral/isar/isar.el and ProofGeneral/isar/find-theorems.el. The latter is new, while only a few lines of the former have been modified to integrate the search form. Please let me know what you think. (Feel free to take a look at the code and improve it if you like, of course.) |
|||
