diff options
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 |