Custom Query (361 matches)
Results (34 - 36 of 361)
Ticket | Owner | Reporter | Resolution | Summary |
---|---|---|---|---|
#172 | fixed | Problem with indentation in Coq mode | ||
Description |
While editing a Coq script proof file, the indentation does not work. In proof-General->Advanced-> Customize ->Proof user options, the Coq script ident option is activated. When I press tab, or M-x indent-according-to-mode, or M-x ident-region, I receive the message "Symbol's value as a variable is void: script-indent" Indentation works well in other mode like Tuareg I'm runing emacs 22.1.1 (i486-pc-linux-gnu, GTK+ Version 2.12.0) with ProofGeneral-3.7pre080117 and The Coq Proof Assistant, version 8.1pl3 (Dec. 2007) |
|||
#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 |
|||
#176 | fixed | Allow isabelle-chosen-logic to be set by variable comment in thy file | ||
Description |
At the moment a comment like (* -*- isabelle-chosen-logic: "HOL-Nominal" -*- *) doesn't work as desired because of the way the program arguments are set only when we change with the menu. Could improve this by using a calculate function like Coq does. |