Opened 17 years ago
Last modified 17 years ago
#141 closed defect
Warnings in proof mode in Coq — at Initial Version
| Reported by: | Evgeny Makarov | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-3.7 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | Evgeny Makarov, courtieu, David Aspinall |
Description
Dear Proof General Developers,
When Coq issues a warning inside a proof, PG shows the warning in the minibuffer, but it does not show the resulting goal.
For example:
Goal True /\ True -> True. intro H. destruct H as [H1 H2 H3].
After the last command, the minibuffer contains "[Coq] Warning: Unused introduction pattern : H3", but the *response* buffer is empty. The same happens if I process
Require Import Setoid. Goal False. setoid_replace False with True.
The minibuffer contains a truncated warning "[Coq] Warning: There are several relations of the carrier 'Prop'. The relation (P", but the response buffer is again empty.
I am not sure what the correct behavior in this case should be (should PG display the warning *and* the goal?), but the goal should probably be displayed.
I am using CVS snapshot of PG updated on September 3, 2007 and Coq trunk 10056.
Thank you, Evgeny
