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.ml | |
| 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.ml')
| -rw-r--r-- | proofs/proof.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 828365798..2aa31cd25 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -435,6 +435,9 @@ module V82 = struct in { Evd.it=List.hd gls ; sigma=sigma } + let top_evars p = + Proofview.V82.top_evars p.state.proofview + let instantiate_evar n com pr = let starting_point = save_state pr in let sp = pr.state.proofview in |