fixed typo in 'leq interpretation uri which enable nice rendering of

coq's le predicate

diff --git a/helm/matita/core_notation.ma b/helm/matita/core_notation.ma
index 88cd759b806390d96c172d9be7e59f5fd84a8029..486e921b5d4ba717bb317976e8ec8736c48def1d 100644 (file)
--- a/helm/matita/core_notation.ma
+++ b/helm/matita/core_notation.ma
@@ -93,7 +93,7 @@ interpretation "binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/
 
 (* relational operators *)
 
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind x y).
+interpretation "natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
 interpretation "real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y).
 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y).
 interpretation "real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y).

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 1bfd5e51e4578f06605d8aeaf6a748f69638860b..0a3f72d4d37d97e6424eb3535147886527b3aef5 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -181,9 +181,6 @@ let _ =
 let _ =
   at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
   Sys.catch_break true;
-  (try
-     gui#loadScript Sys.argv.(1);
-   with Invalid_argument _ -> ());
   if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
     Helm_registry.set "matita.mode" "cicbrowser";
     let browser = MatitaMathView.cicBrowser () in
@@ -195,6 +192,9 @@ let _ =
     browser#load entry
   end else begin  (* matita *)
     Helm_registry.set "matita.mode" "matita";
+    (try
+       gui#loadScript Sys.argv.(1);
+     with Invalid_argument _ -> ());
     gui#main#mainWin#show ();
   end;
   try

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f9171068f2158d07ca7dcc1695ed7a638a57d5d6..cd3571ff4322aad73318565bc53e20a1de8003c9 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -167,10 +167,9 @@ class sequentViewer obj =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
-(*
-    debug_print "load_sequent: dumping MathML to ./prova";
-    ignore (DomMisc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
-*)
+    let name = "sequent_viewer.xml" in
+    prerr_endline ("load_sequent: dumping MathML to ./" ^ name);
+    ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
  end
 
@@ -556,6 +555,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           XmlDiff.update_dom ~from:current_mathml mathml;
           mathView#thaw
       |  _ ->
+          let name = "cic_browser.xml" in
+          prerr_endline ("cic_browser: dumping MathML to ./" ^ name);
+          ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
           mathView#load_root ~root:mathml#get_documentElement;
           current_mathml <- Some mathml);