coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] info_autorewrite
Date: Wed, 19 Oct 2016 15:29:36 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb0-f182.google.com
Ironport-phdr: 9a23:BjaGnB0U9KYuZjFtsmDT+DRfVm0co7zxezQtwd8ZsesfLvad9pjvdHbS+e9qxAeQG96KsbQZ1aGP6P2oGTRZp83e4DZaKN0EfiRGoPtVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaymUrLV2s+wzqW5/4DZK1FDgyP4ardvJj23qx/Qv48Ym90xBLw2z07gqHtJYORbxitBI1uVk16o782w/YVj/icWsvQo8cIGUKTmcIw3SLVZCHItNGVjt56jjgXKUQbavihUaW4RiBcdWwU=

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

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