diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-26 13:25:52 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-26 13:44:53 +0200 |
| commit | 7b1e94365bee6cc984e5f476864ac753e6f46e3a (patch) | |
| tree | ab085a8f95c6a90a323e3df3950c12e09c5e13af /proofs/pfedit.mli | |
| parent | 9de5a59aa6994e8023b9e551b232a73aab3521fa (diff) | |
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.
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 8 |
1 files changed, 8 insertions, 0 deletions
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 : |