X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=872dccace16b0b25d2f8ee1ae6fa6a2ae3df1266;hb=7c123bfb1568f90f37cd667332fbf60d4423b983;hp=8552cbf8629ba98f72086fd58c11d67512bd9d49;hpb=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 8552cbf86..872dccace 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -61,7 +61,7 @@ let run_script is eval_function  =
   | End_of_file
   | CicNotationParser.Parse_error _ as exn -> raise exn
   | exn -> 
-      MatitaLog.error (MatitaExcPp.to_string exn);
+      MatitaLog.error (snd (MatitaExcPp.to_string exn));
       raise exn
 
 let fname () =
@@ -107,8 +107,8 @@ let rec interactive_loop () =
   | End_of_file ->
      print_newline ();
      clean_exit (Some 0)
-  | CicNotationParser.Parse_error (floc,err) ->
-     let (x, y) = CicNotationPt.loc_of_floc floc in
+  | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+     let (x, y) = HExtlib.loc_of_floc floc in
      MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
      interactive_loop ()
   | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop ()
@@ -200,8 +200,8 @@ let main ~mode =
         clean_exit (Some 1)
       else 
         pp_ocaml_mode ()
-  | CicNotationParser.Parse_error (floc,err) ->
-     let (x, y) = CicNotationPt.loc_of_floc floc in
+  | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+     let (x, y) = HExtlib.loc_of_floc floc in
      MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
      if mode = `COMPILER then
        clean_exit (Some 1)