From 7b1e94365bee6cc984e5f476864ac753e6f46e3a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 13:25:52 +0200 Subject: Pfedit.get_current_context refinement (fix #4523) Return the most appropriate evar_map for commands that can run on non-focused proofs (like Check, Show and debug printers) so that universes and existentials are printed correctly (they are global to the proof). The API is backwards compatible. --- proofs/pfedit.ml | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2f5c1d1c2..a515c9e75 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -71,23 +71,34 @@ let get_nth_V82_goal i = with Failure _ -> raise NoSuchGoal let get_goal_context_gen i = - try -let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in -(sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) - with Proof_global.NoCurrentProof -> Errors.error "No focused proof." + let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in + (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context i = try get_goal_context_gen i - with NoSuchGoal -> Errors.error "No such goal." + with Proof_global.NoCurrentProof -> Errors.error "No focused proof." + | NoSuchGoal -> Errors.error "No such goal." let get_current_goal_context () = try get_goal_context_gen 1 - with NoSuchGoal -> + with Proof_global.NoCurrentProof -> Errors.error "No focused proof." + | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) let env = Global.env () in (Evd.from_env env, env) +let get_current_context () = + try get_goal_context_gen 1 + with Proof_global.NoCurrentProof -> + let env = Global.env () in + (Evd.from_env env, env) + | NoSuchGoal -> + (* No more focused goals ? *) + let p = get_pftreestate () in + let evd = Proof.in_proof p (fun x -> x) in + (evd, Global.env ()) + let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength)) -> id,strength,concl -- cgit v1.2.3