Opened 11 years ago
Closed 11 years ago
#468 closed defect (wontfix)
Some notations with periods make PG hang
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | jasongross9+PG@… |
Description
Notation "a . 1" := (proj1_sig a) (at level 10). Check (exist (fun x => x = x) 1 eq_refl) . 1.
Makes PG hang if I try to evaluate to after the 1.
Note: See
TracTickets for help on using
tickets.
Argh, using notation which includes the command terminator is almost inevitably going to confuse the simple regexp-based parsing in PG. I don't see a way to fix this without getting the prover to parse its own input: this is something that more modern interfaces do (Proof General Eclipse and later interfaces have followed this approach).
Unless someone adds support for that in Coq and Emacs Proof General, I don't think this is something that will be fixed, sorry.