better output from main_demod_equalities

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 33e2d14c0866b4044bc1e81542ac804fc9fed953..769f294fd2ef6d2743ef4d925bee4c3191afb3c2 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -26,7 +26,7 @@
 open Printf
 
 open MatitaGtkMisc
-open MatitaTypes
+open GrafiteTypes
 
 (** {2 Initialization} *)
 
@@ -139,18 +139,16 @@ let _ =
       CicNotationParser.print_l2_pattern;
     addDebugItem "dump moo to stderr" (fun _ ->
       let status = (MatitaScript.current ())#status in
-      let moo, metadata = status.moo_content_rev in
+      let moo = status.moo_content_rev in
       List.iter (fun cmd -> prerr_endline
-        (GrafiteAstPp.pp_command cmd)) (List.rev moo);
-      List.iter (fun m -> prerr_endline
-        (GrafiteAstPp.pp_metadata m)) metadata);
+        (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo));
     addDebugItem "print metasenv goals and stack to stderr"
       (fun _ ->
         prerr_endline ("metasenv goals: " ^ String.concat " "
           (List.map (fun (g, _, _) -> string_of_int g)
             (MatitaScript.current ())#proofMetasenv));
         prerr_endline ("stack: " ^ Continuationals.Stack.pp
-          (MatitaTypes.get_stack (MatitaScript.current ())#status)));
+          (GrafiteTypes.get_stack (MatitaScript.current ())#status)));
 (*     addDebugItem "ask record choice"
       (fun _ ->
         HLog.debug (string_of_int