Opened 16 years ago
Closed 16 years ago
#173 closed defect (fixed)
coq indenting mode gets confused by *) in proofs
Reported by: | Jacob Matthews | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-3.7 |
Component: | 2:pg-emacs | Keywords: | coq indentation |
Cc: |
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 *)
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.
Note: See
TracTickets for help on using
tickets.
Thanks for the report. I've added a patch which seems to fix this problem, but the new indent code is pretty hairy, so I'd be grateful for more testing. I'll also ask Pierre to take a look.