The Coq mailing list

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

On 13/04/2016 15:33, Beta Ziliani wrote:
> Actually, I think what I need is an open_constr. Now the question is,
> what do I do with the sigmas? I get one from the goal, and one for each
> open_constr, which one should I use, or how should I combined them?

You're using 8.5 I believe? This open_constr API is quite broken and is
a source of evar leaks, but there is nothing better in that version.
AFAIR, the sigma you get in the open_constr argument is an extension of
the one of the goal, so that you can discard the latter...

PMP

Attachment: signature.asc
Description: OpenPGP digital signature