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 /stm/asyncTaskQueue.ml | |
| 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 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions