diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e0923cda0..be8fbf89d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1002,12 +1002,12 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Proof_type.LtacAtomCall (te,otac) -> quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (dummy_loc,te))) + (Tacexpr.TacAtom (Loc.ghost,te))) ++ (match !otac with | Some te' when (Obj.magic te' <> te) -> strbrk " (expanded to " ++ quote (Pptactic.pr_tactic (Global.env()) - (Tacexpr.TacAtom (dummy_loc,te'))) + (Tacexpr.TacAtom (Loc.ghost,te'))) ++ str ")" | _ -> mt ()) | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> |