The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

Thanks for the update, Pierre. I'm already using the current git HEAD version, and the Ltac debugging support is superb.

~Scott

On Fri, May 13, 2016 at 7:12 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Hi Scot, Excuse my late answer to this message.

Indeed this option should be allowed in C-c C-v. I will adapt the
state-preserving information.

Meanwhile you can put it the file (which is not satisfying I guess).
Note that PG supports debug mode quite well: hit <enter> in the *coq*
buffer and its outpu will be dispatched in *goal* and *response*
buffers (this was implemented lately, take the current git version).

P.

2016-04-25 20:15 GMT+02:00 scott constable <sdconsta AT syr.edu>:
> Hi All,
>
> When I type "C-c C-v Set Ltac Debug ENTER" into PG, I get the following
> error message:
>
> "Command is not state preserving, I won't execute it!"
>
> First, why am I getting this message? In what sense is Ltac debug mode not
> "state preserving"? Second, is there an easier way to enter/exit Ltac debug
> mode than by directly entering the commands into the proof script?
>
> Thanks in advance,
>
> ~Scott Constable