X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaExcPp.ml;h=24981af6bc6e754b4595b9b04614a26b478ea050;hb=c5cee90d95a54db8897a688f0bade4c503d82e15;hp=8888b8dfed312db253a8d2c31b3b11a58b963d7d;hpb=90a9bd0479b78753498625a85a378720cad35437;p=helm.git diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 8888b8dfe..24981af6b 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -117,10 +117,6 @@ 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 - | GrafiteTypes.Option_error ("baseuri", "not found" ) -> - None, - "Baseuri not set for this script. " - ^ "Use 'set \"baseuri\" \"\".' to set it." | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg | CicNotationParser.Parse_error err -> None, sprintf "Parse error: %s" err @@ -151,6 +147,8 @@ let rec to_string = None, "Already defined: " ^ UriManager.string_of_uri s | CoercDb.EqCarrNotImplemented msg -> None, ("EqCarrNotImplemented: " ^ Lazy.force msg) + | MatitaEngine.EnrichedWithLexiconStatus (exn,_) -> + None, "EnrichedWithLexiconStatus "^snd(to_string exn) | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> let loc = match errorll with