diff options
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 -> |