coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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,
"Command is not state preserving, I won't execute it!"
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
Archive powered by MHonArc 2.6.18.