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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/printer.ml | 5 |
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 *) |