diff options
| author | Emilio Jesus Gallego Arias | 2018-10-26 10:05:58 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | bd5689d4e9294d66b3eb4ecdc0af3ad7d65fe52d (patch) | |
| tree | 46b44ee2f005710509ab847e8db7142dd2cf2b13 /plugins/ltac/tactic_debug.ml | |
| parent | 7efaf86882488034e6545505e1eda7d6e1a6ce14 (diff) | |
[coqpp] [ltac] Adapt to removal of imperative proof state.
We add state handling to tactics.
TODO:
- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 52a83a038f..04f3116664 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -370,7 +370,10 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - let sigma, env = Pfedit.get_current_context () in + (* XXX: This hooks into the ExplainErr extension API + so it is tricky to provide the right env for now. *) + let env = Global.env () in + let sigma = Evd.from_env env in Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) |