Custom Query (361 matches)
Results (7 - 9 of 361)
| Ticket | Owner | Reporter | Resolution | Summary |
|---|---|---|---|---|
| #414 | fixed | PG thinks Preterm command is not state-preserving | ||
| Description |
Preterm is not listed in the Coq commands database, so PG incorrectly(?) thinks it is not state-preserving and refuses to execute it from C-c C-v. |
|||
| #415 | fixed | Wrong file mentioned in installation notes | ||
| Description |
In the Installation notes (http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fcoq%2FREADME), the user is warned to "Check the values of coq-tags and coq-prog-name in coq.el to see that they correspond to the paths for coqtop and the library on your system.". Yet coq-prog-name is set in coq-syntax.el, on line 18: "(defcustom coq-prog-name ;; da: moved from coq.el since needed here". |
|||
| #431 | needmoreinfo | "This subproof is complete" appears at bottom of goals | ||
| Description |
After a bulleted subproof has been completed, This subproof is complete, but there are still unfocused goals: appears at the bottom of the goals window. It should either appear at the top, or not at all. |
|||
Note: See TracQuery
for help on using queries.
