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

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.


ProofGeneral-devel mailing list

Reply via email to