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