diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index b4c84cbf6..d80ac79af 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -171,6 +171,9 @@ module V82 : sig val depth : proof -> int val top_goal : proof -> Goal.goal Evd.sigma + + (* returns the existential variable used to start the proof *) + val top_evars : proof -> Evd.evar list (* Implements the Existential command *) val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit |