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/profile_ltac.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/profile_ltac.ml')
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index db7dcfa6ef..3eb049dbab 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -251,7 +251,7 @@ let string_of_call ck = | Tacexpr.LtacVarCall (id, t) -> Names.Id.print id | Tacexpr.LtacAtomCall te -> (Pptactic.pr_glob_tactic (Global.env ()) - (Tacexpr.TacAtom (Loc.tag te))) + (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, _) -> pr_glob_constr_env (Global.env ()) c | Tacexpr.LtacMLCall te -> |