More compact disambiguation errors.

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 33e2d14c0866b4044bc1e81542ac804fc9fed953..efaaa57074fe0d71261321426daaa3bfac2b70cd 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} *)
 
@@ -41,7 +41,6 @@ let script =
   let s = 
     MatitaScript.script 
       ~source_view:gui#sourceView
-      ~init:(Lazy.force MatitaEngine.initial_status) 
       ~mathviewer:(MatitaMathView.mathViewer ())
       ~urichooser:(fun uris ->
         try
@@ -139,18 +138,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