coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Easy way to enter Ltac debug mode in PG?

From: scott constable <sdconsta AT syr.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Easy way to enter Ltac debug mode in PG?
Date: Mon, 25 Apr 2016 14:15:40 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
Ironport-phdr: 9a23:kQgayxZUA3VwzoQCiupqXmz/LSx+4OfEezUN459isYplN5qZpc+9bnLW6fgltlLVR4KTs6sC0LqG9f++EjVZsN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDivcKNKFwR1XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzANmR1UH0DO6xfhQp77tiay4vFx0y6cJtH/ZaslQ3Kv47o9G0ygszsOKzNsqDKfscd3lq8O+B8=

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

[Coq-Club] Easy way to enter Ltac debug mode in PG?, scott constable, 04/25/2016
- Re: [Coq-Club] Easy way to enter Ltac debug mode in PG?, Clément Pit--Claudel, 04/25/2016