X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=3c141126d3c26f8c80be266fc8e18588c42016b4;hb=39320e6e7bfe3278598278398389854bd721f756;hp=6ca72083008975c8365198a06225325cdc0d8807;hpb=badc43296cdc81e4376abe72071941317effe8b3;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 6ca720830..3c141126d 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -25,7 +25,8 @@ let tactic_of_ast = function
       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Intros (_, Some num, names) ->
       (* TODO Zack implement intros length *)
-      PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
+      PrimitiveTactics.intros_tac ~howmany:num
+        ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
@@ -335,7 +336,6 @@ let eval_command status cmd =
         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") 
       in
       let metasenv = MatitaMisc.get_proof_metasenv status in
-      debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body);
       let (body_type, ugraph) =
         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
       in