diff options
| author | Maxime Dénès | 2017-11-21 22:24:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-21 22:24:59 +0100 |
| commit | eb91ccaf236bc9a60a1e216b76a0a42980c072a7 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /plugins/ltac/tactic_debug.ml | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
| parent | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (diff) | |
Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index a669692fc9..2dd7c9a747 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -20,7 +20,9 @@ let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp let prmatchrl rl = Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) - (fun (_,p) -> Printer.pr_constr_pattern p) rl + (fun (_,p) -> + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -369,7 +371,8 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) + let sigma, env = Pfedit.get_current_context () in + Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) in |