debian: rebuilt against ocaml 3.08.3

[helm.git] / helm / matita / matita.ml

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index e6eff09fec2bea1060f73012f6d207d6681542e2..3052e975e5cab70b78f8a86f7137bba1cda31738 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -95,7 +95,6 @@ let console_callback s =
     | tac -> tac
   in
   let needed_by_script ast =
-    prerr_endline (TacticAstPp.pp_tactical ast);
     match strip_locations ast with
     | A.Tactic _
     | A.Command
@@ -104,8 +103,9 @@ let console_callback s =
     | _ -> false
   in
   let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in
+  debug_print (sprintf "evaluating '%s'" s);
   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 (); *)