X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=59ec55f3a2714ce82c1ba67db6d4e1f7b211a876;hb=81ad82070892b2f2740111d97b2d72394f969328;hp=e6eff09fec2bea1060f73012f6d207d6681542e2;hpb=642e20a0135126586603ffb539f0d1c1428f1502;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index e6eff09fe..59ec55f3a 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -105,7 +105,7 @@ let console_callback s =
   in
   let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in
   if needed_by_script ast then
-    script#advance ast
+    script#advance s
   else
     interpreter#evalAst ast
 
@@ -138,8 +138,7 @@ let _ =
   let hole = CicAst.UserInput in
   let tac ast _ =
     let ast = A.Tactic ast in
-    ignore (interpreter#evalAst ast);
-    ignore (script#advance ast)
+    ignore (script#advance (TacticAstPp.pp_tactical ast))
   in
   let tac_w_term ast _ =
 (*     gui#console#clear (); *)