Custom Query (361 matches)
Results (58 - 60 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #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". |
|||
| #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". |
|||
| #417 | fixed | Website states wrong minimal emacs version | ||
| Description |
http://proofgeneral.inf.ed.ac.uk/download#prereq says that emacs 23.1 or later is required, but 4.1RC2 requires version 23.3 or later: In toplevel form: coq/coq.el:443:24:Error: reference to free variable `smie-rules-function' make[1]: *** [coq/coq.elc] Error 1 |
|||
Note: See TracQuery
for help on using queries.
