diff options
| author | aspiwack | 2011-11-23 17:09:11 +0000 |
|---|---|---|
| committer | aspiwack | 2011-11-23 17:09:11 +0000 |
| commit | 7b2bf4785916803c24629239aa746706fe3f6ef6 (patch) | |
| tree | 9cd8d1a87e6a0f9ba7f624f1feaf89b4e1952abf /proofs | |
| 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')
| -rw-r--r-- | proofs/proof.ml | 3 | ||||
| -rw-r--r-- | proofs/proof.mli | 3 | ||||
| -rw-r--r-- | proofs/proofview.ml | 6 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 |
4 files changed, 15 insertions, 0 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 8283657983..2aa31cd253 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 diff --git a/proofs/proof.mli b/proofs/proof.mli index b4c84cbf60..d80ac79af2 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 diff --git a/proofs/proofview.ml b/proofs/proofview.ml index b76c802dfd..0d50d521f3 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -484,6 +484,12 @@ module V82 = struct let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in { Evd.it = goals ; sigma=solution } + let top_evars { initial=initial } = + let evars_of_initial (c,_) = + Util.Intset.elements (Evarutil.evars_of_term c) + in + List.flatten (List.map evars_of_initial initial) + let instantiate_evar n com pv = let (evk,_) = let evl = Evarutil.non_instantiated pv.solution in diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 25a58a482a..24da9d77b3 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -200,6 +200,9 @@ module V82 : sig val goals : proofview -> Goal.goal list Evd.sigma val top_goals : proofview -> Goal.goal list Evd.sigma + + (* returns the existential variable used to start the proof *) + val top_evars : proofview -> Evd.evar list (* Implements the Existential command *) val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview |