Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Debugging autorewrite

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Debugging autorewrite


Chronological Thread 
  • From: Andrej Bauer <andrej.bauer AT andrej.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Debugging autorewrite
  • Date: Mon, 17 Sep 2012 10:16:44 -0400

With passage from 8.3 to 8.4 an autorewrite with a hint database loops
on me. What is a reasonable way of debugging this? I would like to see
"one step" of autorewrite, that would already help a lot. I apologize
if this is an FAQ, I did look around before asking.

With kind regards,

Andrej


  • [Coq-Club] Debugging autorewrite, Andrej Bauer, 09/17/2012

Archive powered by MHonArc 2.6.18.

Top of Page