Opened 12 years ago
Closed 12 years ago
#445 closed defect (worksforme)
Proof General (or coqtop?) barfs on "Arguments foo / ..."
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.2 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | jasongross9+bugzilla@… |
Description
When I make a new file containing the two (literal) line
Definition foo a : Type := a. Arguments foo / ...
and try to evaluate it when running Coq 8.4beta2, PG accepts the first line fine (highlights it blue), highlights the second line pink, marks it as read-only, and refuses to do anything more with Coq; it refuses to stop coq with ctrl+c, ctrl+c, it gives me the following error when I try to retract the buffer and start over:
proof-add-to-queue: Assertion failed: (eq proof-shell-busy queuemode)
and it never finishes evaluating the line (where never >= 15 seconds). Given that coqtop sits there using 0% CPU and 8 MB of RAM, and coqc errors and quits after 2s, I'm inclined to think that this is either a PG problem, or a communication problem.
I can't reproduce this bug. This is working correctly with my cvs version (with coq trunk and coq 8.4). Has it been fixed?
Definition foo a : Type := a. Arguments foo / .
Print foo.