coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Version of vm_compute that ignores opaque?

From: Gregory Malecha <gmalecha AT cs.harvard.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Version of vm_compute that ignores opaque?
Date: Fri, 6 Feb 2015 10:52:21 -0800

Hello --

I have a bunch of proofs that I have Qed'd and now I want to reduce them, just to see what they look like after being fully reduced. Is there any easy way to do this or do I need to search/replace Qed with Defined?

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

[Coq-Club] Version of vm_compute that ignores opaque?, Gregory Malecha, 02/06/2015
- Re: [Coq-Club] Version of vm_compute that ignores opaque?, Maxime Dénès, 02/06/2015
  - Re: [Coq-Club] Version of vm_compute that ignores opaque?, Enrico Tassi, 02/06/2015