Custom Query (361 matches)
Results (22 - 24 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #159 | wontfix | Goal centering | ||
| Description |
Is it possible to have the centering behavior of the *goals* window be configurable? I see from ticket #111 that the behavior was changed recently to center on the bottom of the goal instead of the top of the hypotheses, but unfortunately a lot of things I prove end up with 50 line goals, so the old behavior (while sometimes not ideal) is still better for me. |
|||
| #204 | fixed | undo stops undoing in large proofs | ||
| Description |
In large Coq proofs (with more than 100 lines), undo stops working. For instance: Lemma Foo : True. idtac. [repeat "idtac." around another 112 times] assert (NI : ~False). intros IX; auto. (* Process the script until here, then undo back 3 or 4 lines.
|
|||
| #296 | fixed | PG accepts garbage though Coq said "illegal begin of vernac" | ||
| Description |
If I type the following complete garbage and press "C-c C-RET" at the end of the line, Proof General accepts it, even though I see in the *coq* buffer that Coq has said "illegal begin of vernac": Check nat.&!&*\:,.:<*&^!)@)$. I'm guessing that Proof General doesn't recognize the first period as a command separator and there's a miscommunication between Coq and Proof General regarding how much of the text was processed. I'm using GNU Emacs 23.1.1 and Proof General 3.7.1, though I checked that the problem still exists in the latest Proof General from CVS. |
|||
