1. matitaEngine splitted into disambiguation (now in grafite_parser) and

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 33e2d14c0866b4044bc1e81542ac804fc9fed953..0a83b737ebe54e7ee4dd7db23c9bd1eb824bd0e1 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} *)
 
@@ -141,7 +141,7 @@ let _ =
       let status = (MatitaScript.current ())#status in
       let moo, metadata = status.moo_content_rev in
       List.iter (fun cmd -> prerr_endline
-        (GrafiteAstPp.pp_command cmd)) (List.rev moo);
+        (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo);
       List.iter (fun m -> prerr_endline
         (GrafiteAstPp.pp_metadata m)) metadata);
     addDebugItem "print metasenv goals and stack to stderr"
@@ -150,7 +150,7 @@ let _ =
           (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