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 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6e5b048cc..4c733dd4f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -485,9 +485,7 @@ let ppist ist = (* Vernac-level debugging commands *) let in_current_context f c = - let (evmap,sign) = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in + let (evmap,sign) = Pfedit.get_current_context () in f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*) (* We expand the result of preprocessing to be independent of camlp4 |