diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-23 17:09:11 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-23 17:09:11 +0000 |
| commit | 7b2bf4785916803c24629239aa746706fe3f6ef6 (patch) | |
| tree | 9cd8d1a87e6a0f9ba7f624f1feaf89b4e1952abf /proofs/proof.mli | |
| parent | 45b6c77dfd819bf64283146859aac56faac49ead (diff) | |
In emacs mode, prints a list of the dependent existential variables introduced
during the proof together with information whether they were (partially)
instantiated and if it's the case the list of existential variables that were
used to that effect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14721 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |