Opened 15 years ago
Closed 15 years ago
#268 closed defect (fixed)
Hiding proofs wrong with Coq
| Reported by: | courtieu | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.0 |
| Component: | 2:pg-emacs | Keywords: | hiding proof |
| Cc: | greenrd@… |
Description
Hi,
When using PG with Coq, several bugs happen:
1) comments disappear 2) modules disappear 3) section disappear 4) it is not possible to deactivate proof hiding (by menu or by hand or by contextual menu, proofs remain hidden)
Change History (4)
comment:1 Changed 15 years ago by
comment:2 Changed 15 years ago by
The same happens to me (proofs disappear after processing Qed). I use GNU Emacs 23.0.91.1 and ProofGeneral 4.0pre090416. This happens even with the minimal .emacs file containing one line: (load-file "~/ProofGeneral/generic/proof-site.el"). The variable proof-disappearing-proofs is nil, and the option Disappearing Proofs is unchecked.
Evgeny
comment:3 Changed 15 years ago by
| Cc: | greenrd@… added |
|---|
I also see this. It is possible to disable disappearing proofs for the current session, but I'm not sure how I managed to do it.
comment:4 Changed 15 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
Should be fixed now in CVS. Thanks for reports.
Sorry, I did not say that this happens in cvs version of pg, it seems ok in PG-3.7.1.