Custom Query (361 matches)
Results (55 - 57 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#173 | fixed | coq indenting mode gets confused by *) in proofs | ||
Description |
Using the latest CVS version of pg-emacs (as of Thu Jan 24 16:48:42 PST 2008), enter the following Coq script: Theorem p : forall (P : Prop), P -> P. Proof. try (simpl in *). intros P H. apply H. Qed.
This is legal Coq code, but the occurrence of the sequence |
|||
#449 | fixed | coq electric terminator conflict | ||
Description |
The new addition (define-key coq-mode-map (kbd ".") 'coq-colon-self-insert) hides the generic default (proof-electric-terminator) and there is no configure option. Hendrik |
|||
#437 | fixed | compilation error with LANG=C | ||
Description |
Hi, with setting
compilation of phox/phox-pbrpm.el fails with In toplevel form: phox/phox-pbrpm.el:316:1:Error: Args out of range: "C", 0, 2 make[1]: * [phox/phox-pbrpm.elc] Error 1 make[1]: Leaving directory `/home/tews/src/pg' make: * [compile] Error 2 |