coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] info_autorewrite

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] info_autorewrite
Date: Wed, 19 Oct 2016 22:02:19 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f180.google.com
Ironport-phdr: 9a23:NR1CSxalUxPvB9HpNcD5NVv/LSx+4OfEezUN459isYplN5qZpsS4bnLW6fgltlLVR4KTs6sC0LuM9f2/EjReqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjnLparRraR6ysA/5t88MgIIkJLxnmTXTpX4dXu1K2WNpKE/bpBHu686ttMpm+jhMsvcJ8sdcTaz/OaMiQuoLX3wdL2kp6Ziz5lH4RgyV6y5EXw==

I don't think there is now. It shouldn't be too hard to implement though.

On Wed, 19 Oct 2016 at 21:30, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Is there a way to get autorewrite to output the rewrites that it invoked?
For maintainability of my Coq developments, I usually replace the contents
of eauto with the output of info_eauto. I wish there was an info_autorewrite tactic
that would allow me to do the same with autorewrite.
Also, this would be helpful to find out the items in a rewrite database that cause
autorewrite to misbehave.

Similar questions have been asked before (e.g. https://sympa.inria.fr/sympa/arc/coq-club/2012-09/msg00056.html) but never received any response.

-- Abhishek
http://www.cs.cornell.edu/~aa755/

[Coq-Club] info_autorewrite, Abhishek Anand, 10/19/2016
- Re: [Coq-Club] info_autorewrite, Matthieu Sozeau, 10/20/2016