X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaExcPp.ml;h=076a5d763e6fccd1cb4fe0ae4055eca99399e713;hb=910c252965fe17d6b5af92e4658e7d02bac82d58;hp=8888b8dfed312db253a8d2c31b3b11a58b963d7d;hpb=90a9bd0479b78753498625a85a378720cad35437;p=helm.git

diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml
index 8888b8dfe..076a5d763 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\" \"<uri>\".' to set it."
   | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg
   | CicNotationParser.Parse_error err ->
       None, sprintf "Parse error: %s" err
@@ -149,8 +145,10 @@ let rec to_string =
      None, "Type checking assertion failed: " ^ Lazy.force msg
   | LibrarySync.AlreadyDefined s -> 
      None, "Already defined: " ^ UriManager.string_of_uri s
-  | CoercDb.EqCarrNotImplemented msg ->
-     None, ("EqCarrNotImplemented: " ^ Lazy.force msg)
+  | DisambiguateChoices.Choice_not_found msg ->
+     None, ("Disambiguation choice not found: " ^ Lazy.force msg)
+  | MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->
+     None, "EnrichedWithLexiconStatus "^snd(to_string exn)
   | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
      let loc =
       match errorll with