diff options
| author | Matthieu Sozeau | 2016-05-26 13:25:52 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-05-26 13:44:53 +0200 |
| commit | 7b1e94365bee6cc984e5f476864ac753e6f46e3a (patch) | |
| tree | ab085a8f95c6a90a323e3df3950c12e09c5e13af /_CoqProject | |
| 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 '_CoqProject')
0 files changed, 0 insertions, 0 deletions