The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Feb 06, 2015 at 08:28:24PM +0100, Maxime Dénès wrote:
> 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.

I think the right fix would be to have a vernacular command that turns a
Qed-opaque term into a transparent one.  That would mean the STM (the
scheduler for asynchronously processed proof Coq 8.5 features) would
_statically_ know when an opaque proof term becomes transparent, and
make the switch a synchronization point.  Unfortunately I had no time to
code it.

Simply making a tactic bypass opaque proofs is not going to work well in
8.5.  In particular if the opaque proof belongs to a Required .vio file
(a .v file that was compiled with the -quick option) you get an error,
since .vio files don't contain proof terms.  It works well if the opaque
proof in question is in the same file of the call to vm_compute, or if
it belongs to a Required .vo file.

It may be just a matter of producing a good error message in the .vio
case, inviting the user to turn the .vio into a (complete) .vo file and
then retry.  A vernacular making this error message unnecessary is
a nicer solution, but requires some additional work.

Best,
-- 
Enrico Tassi