Just to note, I'm adding a configuration option to force the use of the
existing Emacs mode, so Prooftree will always be available.

-- Paul
On May 13, 2016 11:08, "Pierre Courtieu" <pierre.court...@cnam.fr> wrote:

> 2016-05-13 9:49 GMT+02:00 Hendrik Tews <hendrik.t...@fireeye.com>:
> > For 2 and 5 I insert additional print commands into the queue of
> > commands. Because you cannot print wrt. an old state, these print
> > commands need to be inserted directly after the command that
> > generates additional subgoals or that instantiate existential
> > variables.
>
> This might change with the idesave + Stm protocol.
>
> Paul are you using the Stm stuff?
>
> P.
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to