Custom Query (361 matches)
Results (73 - 75 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #416 | fixed | Emacs indentation can go into an infinite loop | ||
| Description |
Paste the following code in. After the final period, press either Ctrl+J or enter followed by tab. Emacs (Aquamacs or GNU Emacs 23) will spin up one processor to 100% and run forever. Theorem binaryUnaryCommute' : forall b : bin, convert (succ (b)) = convert b + 1. Proof. intros b. induction b as [| b' | b']. Case "b = BO". |
|||
| #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". |
|||
| #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. |
|||
Note: See TracQuery
for help on using queries.
