diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 7c538cf0e..15ee7cf06 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -178,6 +178,10 @@ module V82 : sig (* returns the existential variable used to start the proof *) val top_evars : proof -> Evd.evar list + (* Turns the unresolved evars into goals. + Raises [UnfinishedProof] if there are still unsolved goals. *) + val grab_evars : proof -> unit + (* Implements the Existential command *) val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit end |