Custom Query (361 matches)

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)

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 *) seems to confuse the indenter --- hitting tab with the point on the beginning of the second or third lines gives the Emacs error message "Invalid search bound (wrong side of point)" and hitting tab with the point on a fifth (blank) line gives the Emacs error message "Wrong type argument: integer-or-marker-p, nil". Removing the try (simpl in *) or changing it to something that doesn't have a *) in it --- e.g., try (simpl in *; idtac) --- makes the problem go away.

When using ProofGeneral with XEmacs 21.4 and the CVS version of Isabelle, it is not possible to exit the prover by selecting the "Isabelle -> Exit Isabelle" menu item. Instead of terminating the prover, ProofGeneral just displays the message "Warning: buffer *isabelle* not killed; still associated with prover process.". This problem does not occur with XEmacs 21.5, though.