The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 2016-04-25 14:15, scott constable wrote:
> First, why am I getting this message? In what sense is Ltac debug
> mode not "state preserving"?

I think this is Coq Proof General being too conservative. It pretty crudely 
checks that you're not setting options with ‘C-c C-v’, since it could lead to 
confusing results (it's fine to issue a ‘Show’ command, for example, but not 
a ‘Set Default Timeout’, or a ‘Hint’, etc.). Set Ltac Debug is special in the 
sense that backtracking to a point before it doesn't disable it, so it should 
always be safe to issue (unlike most other options).

I'm not aware of a good way for Proof General to check whether an option is 
state preserving or not, unfortunately.

> Second, is there an easier way to enter/exit Ltac debug mode than by
> directly entering the commands into the proof script?

You could disable that check by customizing ‘proof-strict-state-preserving’.

Cheers,
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature