diff options
| author | Matthieu Sozeau | 2016-05-26 13:25:52 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-05-26 13:44:53 +0200 |
| commit | 7b1e94365bee6cc984e5f476864ac753e6f46e3a (patch) | |
| tree | ab085a8f95c6a90a323e3df3950c12e09c5e13af /stm | |
| 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 'stm')
| -rw-r--r-- | stm/lemmas.ml | 10 | ||||
| -rw-r--r-- | stm/lemmas.mli | 1 |
2 files changed, 1 insertions, 10 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index fb64a10c6c..5b205e79ef 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -509,13 +509,5 @@ let save_proof ?proof = function (* Miscellaneous *) let get_current_context () = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> - try (* No more focused goals ? *) - let p = Pfedit.get_pftreestate () in - let evd = Proof.in_proof p (fun x -> x) in - (evd, Global.env ()) - with Proof_global.NoCurrentProof -> - let env = Global.env () in - (Evd.from_env env, env) + Pfedit.get_current_context () diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 16e54e318e..ca6af9a3fa 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -60,4 +60,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni and the current global env *) val get_current_context : unit -> Evd.evar_map * Environ.env - |