]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaExcPp.ml
1. matitaEngine splitted into disambiguation (now in grafite_parser) and
[helm.git] / helm / matita / matitaExcPp.ml
index fcb02234577fe85e9b16cb74d2bb27cd547127e0..d58ceaf7a45c952d916b91539c26b78ddcf3e67d 100644 (file)
@@ -31,11 +31,11 @@ let rec to_string =
       let _,msg = to_string exn in
       let (x, y) = HExtlib.loc_of_floc floc in
        Some floc, sprintf "Error at %d-%d: %s" x y msg
-  | MatitaTypes.Option_error ("baseuri", "not found" ) -> 
+  | GrafiteTypes.Option_error ("baseuri", "not found" ) -> 
       None,
       "Baseuri not set for this script. "
       ^ "Use 'set \"baseuri\" \"<uri>\".' to set it."
-  | MatitaTypes.Command_error msg -> None, "Error: " ^ msg
+  | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
   | CicNotationParser.Parse_error err ->
       None, sprintf "Parse error: %s" err
   | UriManager.IllFormedUri uri -> None, sprintf "invalid uri: %s" uri