X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=69334355fc6e60b4c4163276f74e134d72f5de13;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=acb73fb54909f90da93c260e12b201798c9b15d2;hpb=642e20a0135126586603ffb539f0d1c1428f1502;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index acb73fb54..69334355f 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -114,7 +114,7 @@ class script ~(interpreter:MatitaTypes.interpreter) () =
       gui#main#showScriptMenuItem#set_active true
 
     method advance tactical =
-      let text = "\n" ^ TacticAstPp.pp_tactical tactical in
+      let text = "\n" ^ tactical in
       buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) text;
       let res = self#_forward () in
       if not (fst res) then begin