]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMathView.ml
* Part of matita that used to deal with the library moved into ocaml/library
[helm.git] / helm / matita / matitaMathView.ml
index 7a54049a87a251c4b6f99328f067e4a9698fc8c8..15a4a126d047384c86ef6f483f879f524fbe8dce 100644 (file)
@@ -341,7 +341,7 @@ object (self)
       | Some ((None, _, _, _, _, _) as info) ->
           (* building a dummy sequent for obj *)
           let t = self#find_obj_conclusion id in
-          MatitaLog.debug (CicPp.ppterm t);
+          HLog.debug (CicPp.ppterm t);
           info, (~-1, [], t)
       | None -> assert false
     in
@@ -397,7 +397,7 @@ object (self)
         ids_to_terms, ids_to_hypotheses, ids_to_father_ids,
         Hashtbl.create 1, None));
     let name = "sequent_viewer.xml" in
-    MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+    HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
     ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
 
@@ -417,7 +417,7 @@ object (self)
         self#thaw
     |  _ ->
         let name = "cic_browser.xml" in
-        MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+        HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
         ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
         self#load_root ~root:mathml#get_documentElement;
         current_mathml <- Some mathml);