diff options
Diffstat (limited to 'contrib/interface/blast.ml')
| -rwxr-xr-x | contrib/interface/blast.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 78716435c1..f7f6674e87 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -595,7 +595,7 @@ let blast_tac display_function = function let blast_tac_txt = blast_tac - (function x -> msgnl(Pptacticnew.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));; + (function x -> msgnl(Pptactic.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));; (* Obsolète ? overwriting_add_tactic "Blast1" blast_tac_txt;; |