Hendrik Tews <t...@os.inf.tu-dresden.de> writes: - support for braces and bullets
This requires more work than I thought. I have to postpone this to October. Given that only few people use braces/bullets (because they are new) and even fewer use Prooftree, it doesn't make sense to delay the release of Proof General because of this issue. The problem is that with braces and bullets Coq exhibits a state where the old current goal has been finished but it has not yet switched to the next goal. Without braces and bullets you never see such a state and therefore all prooftree code assumes that such a state is not visible. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
