Custom Query (361 matches)
Results (55 - 57 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #141 | worksforme | Warnings missing in proof mode in Coq | ||
| 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 |
|||
| #143 | fixed | Add XML/PGIP test scripts to Isabelle/Admin distribution | ||
| #152 | fixed | Faults with main regexps in XEmacs 21.5(b28) for Coq | ||
| Description |
The above version of XEmacs (standard XEmacs on Fedora 7) has problems with matching ends of commands properly. It trips up on the standard test |
|||
