diff options
| author | Emilio Jesus Gallego Arias | 2018-11-05 02:51:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 05:29:50 +0100 |
| commit | 4949b991019dd6dd845627cc03e800072bc7ed10 (patch) | |
| tree | 6d77ed011a33e2afdcd544ff301aa84a2056f9d2 /plugins/ltac/tactic_debug.ml | |
| parent | f8a76b3d383abf468fb21df509f5da8f8aafa913 (diff) | |
[ltac] Use CAst nodes in the tactic AST.
This provides several advantages to people serializing tactic
scripts. Appearance of the involved constructors is common enough as
to bother to submit this PR.
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 6bab8d0353..877d4ee758 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -365,7 +365,7 @@ let explain_ltac_call_trace last trace loc = Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.tag te))) + (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then |