Custom Query (361 matches)
Results (28 - 30 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#109 | fixed | Missing output from Coq | ||
Description |
Dear Proof General developers, In Coq, the identity tactic, idtac, is also used to print its arguments, for example, for debugging purposes. However, I don't see the output of idtac either in the *goals* or in the *response* buffer. For example, I don't see any output after executing the following script: Goal True. idtac "Hello!". Is there a way to correct this? Thank you, Yeveniy Makarov Emacs : GNU Emacs 21.4.1 (i386-redhat-linux-gnu, X toolkit, Xaw3d scroll bars) of 2006-03-07 on hs20-bc1-6.build.redhat.com Package: Proof General current state: ============== (setq proof-general-version "Proof General Version 3.6pre061027. Released by da." proof-assistant "Coq" ) |
|||
#110 | fixed | Search Rewrite and Search About queries for Proof General/Coq | ||
Description |
The options "Search Rewrite ..." and "Search About ..." do not work in the pre-release (ProofGeneral-3.7pre070312) To fix the problem I had to patch the file coq.el. I include the corrected version. |
|||
#111 | fixed | Centering the goal window on the right part of the goals | ||
Description |
In coq, when doing large proofs, the goals window tends to not be centered on the right information: it only shows the oldest assumptions, and when the list of assumption is too long, it does not even show the statement of the first goal.
I suggest centering on bar of equal signs that separates the most recent hypotheses from the current goal. I did it by modifying two files: proof-utils.el and pg-goals.el
While I think that the modification on proof-utils.el can be shared with other proof
systems (I only add the possibility that the target point could be given by a string
that will be searched in the buffer), the change done on pg-goals.el is coq-specific
and should not be left there, but I could not find how to make the code customizable in this respect. So this is a suggestion for modification, but this should be reviewed to make it more generic in its approach. |