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.mli | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index cd8992015..cfab8bd63 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -93,6 +93,14 @@ val get_goal_context : int -> Evd.evar_map * env val get_current_goal_context : unit -> Evd.evar_map * env +(** [get_current_context ()] returns the context of the + current focused goal. If there is no focused goal but there + is a proof in progress, it returns the corresponding evar_map. + If there is no pending proof then it returns the current global + environment and empty evar_map. *) + +val get_current_context : unit -> Evd.evar_map * env + (** [current_proof_statement] *) val current_proof_statement : -- cgit v1.2.3