diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index e8faf862f..b7d88bf02 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -483,7 +483,7 @@ let fmt_autotactic = (str"apply " ++ prterm c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> - (str "(external) " ++ Pptacticnew.pr_glob_tactic (Global.env()) tac) + (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) let fmt_hint v = (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ()) |