X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Fmatita.ml;h=0086f6aeac3f5a48860d13f358837191ee4912d9;hb=78229b5b53f947df657547e682c5365bbba9455b;hp=efaaa57074fe0d71261321426daaa3bfac2b70cd;hpb=41be5e85a1103a5b14495bb487995a6a88e79c48;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index efaaa5707..0086f6aea 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -117,9 +117,9 @@ let _ =
       List.iter (fun (u,_,_) -> 
         prerr_endline (UriManager.string_of_uri u)) 
         (CicEnvironment.list_obj ()));
-    addDebugItem "print selections" (fun () ->
+(*     addDebugItem "print selections" (fun () ->
       let cicMathView = MatitaMathView.cicMathView_instance () in
-      List.iter HLog.debug (cicMathView#string_of_selections));
+      List.iter HLog.debug (cicMathView#string_of_selections)); *)
     addDebugItem "dump script status" script#dump;
     addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
       Helm_registry.save_to "./foo.conf.xml");
@@ -139,8 +139,11 @@ let _ =
     addDebugItem "dump moo to stderr" (fun _ ->
       let status = (MatitaScript.current ())#status in
       let moo = status.moo_content_rev in
-      List.iter (fun cmd -> prerr_endline
-        (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo));
+      List.iter
+        (fun cmd ->
+          prerr_endline (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false)
+            cmd))
+        (List.rev moo));
     addDebugItem "print metasenv goals and stack to stderr"
       (fun _ ->
         prerr_endline ("metasenv goals: " ^ String.concat " "