aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/printer.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 8469490f0..ac20eeb6f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -28,10 +28,7 @@ let delayed_emacs_cmd s =
if !Flags.print_emacs then s () else str ""
let get_current_context () =
- try Pfedit.get_current_goal_context ()
- with e when Logic.catchable_exception e ->
- let env = Global.env () in
- (Evd.from_env env, env)
+ Pfedit.get_current_context ()
(**********************************************************************)
(** Terms *)