Custom Query (361 matches)
Results (61 - 63 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #430 | fixed | Make "Set Ltac Debug" work | ||
| Description |
When Proof General attempts to handle compound tactics in debug mode, it freezes. If you switch to the *coq* buffer, you find that Coq has switched into an interactive mode, but there is no indication of this in the UI. |
|||
| #428 | fixed | subsubsection links not working in PG doc | ||
| Description |
Hi, in the Proof General documentation at http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+user+manual&file=releases%2FProofGeneral%2Fdoc%2FProofGeneral%2FProofGeneral_11.html#Multiple-File-Support the link for "Current Limitations", pointing to subsubsection 10.2.4 does not work. The other links for subsubsections do not work as well. The text of these subsubsections is present and on http://proofgeneral.inf.ed.ac.uk/userman the link to 10.2.4 _does_ work. If I compile the documentation myself and view it on the hard disk, the links do also work. Bye, Hendrik |
|||
| #427 | duplicate | defpacustom and undo | ||
| Description |
Hi, defpacustom settings are not preserved over undo, at least not for Coq. Consider, for instance, switching "Print fully explicit" on in the middle of some file, then after undo, you get again normal printing behavior. (For Coq, this is of course not really surprising.) I don't know, if we really want to implement settings that are preserved over undo. However, it would be nice, if the defpacustom variable is reset to normal state (and thereby also its menu entry), if its effect is lost because of an undo. Hendrik |
|||
