diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-03-25 16:46:50 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-03-25 16:55:06 +0100 |
| commit | 7e7b5684d8f8066b90fca3395104af7241b8aed6 (patch) | |
| tree | 2d5f220f65eee3cca3a856bf823103d07e8aefc3 /printing/printer.ml | |
| parent | 25c6356326773ac56380b81de6f58d15caae8680 (diff) | |
Univs: fix get_current_context (bug #4603, part I)
Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 63755d7ff..4e740bffe 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -30,7 +30,8 @@ let delayed_emacs_cmd s = let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) + let env = Global.env () in + (Evd.from_env env, env) (**********************************************************************) (** Terms *) |