Opened 9 years ago
Closed 9 years ago
#503 closed defect (fixed)
Some coq output get lost for query processed just after an error stops the queue.
| Reported by: | courtieu | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: |
Description
To reproduce:
Check nat. (* 1 *) Check foo. (* 2 *)
Check nat. (* 3 *)
1) process *directly* to (*2*), for example with C-c c-b. 2) query something, f.ex. C-c C-a C-c RET eq RET 3) nothing appears.
Change History (2)
comment:1 Changed 9 years ago by
comment:2 Changed 9 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
This was an old bug. Fixed by "stop silent" checking when adding something to the queue in the generic code.
Hopefully this will not break other prover's code.