The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi Greg,

As far as I know, you'll have to search/replace. There is only a very
limited number of vernacular commands / tactics that can bypass
Qed-style opacity, like Print, Print Assumptions and extraction.

Writing a patch for vm_compute that ignores opacity wouldn't be too
hard, though.

Cheers,

Maxime.

On 02/06/2015 07:52 PM, Gregory Malecha wrote:
> 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?
>