The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 09/03/2013 21:31, AUGER Cédric wrote:
> There are some printed terms which cannot be parsed by Coq, even with
> deactivating Notations, implicit arguments and in fact in asking to
> print absolutely all stuff. I have no example, but I once find some.
> I know I posted it here on the mailing list but it was a very long time
> ago. That said it is not often I find such a term.

I've quickly hacked a proof of concept using Unix.fork and darkest magic 
to bypass this type of problem. The tactic sends back the proof term 
through a pipe using OCaml Marshal module. This is ugly and really 
unsafe, but this should work.

Currently, the tactic only displays the list of proof-term as a 
proof-of-concept (no pun intended), so you're still having the problem 
of solving the goals. Nevertheless one should be able to instantiate a 
goal with this list, but I still don't know how to instantiate all evars 
representing a goal at once (any avice, Arnaud?).

PMP

Attachment: fork.tar.gz
Description: application/gzip