fix

[helm.git] / helm / matita / matitaExcPp.ml

diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml
index 29f08d514980cdfea95218be2f06a7ebf400a1c3..e9e7f488f3ff731c1d9e3ff0fc496f2d9a18a56b 100644 (file)
--- a/helm/matita/matitaExcPp.ml
+++ b/helm/matita/matitaExcPp.ml
@@ -63,10 +63,10 @@ let rec to_string =
      None, "Type checking assertion failed: " ^ Lazy.force msg
   | LibrarySync.AlreadyDefined s -> 
      None, "Already defined: " ^ UriManager.string_of_uri s
-  | MatitaDisambiguator.DisambiguationError (offset,errorll) ->
+  | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
      let rec aux n ?(dummy=false) (prev_msg,phases) =
       function
-         [] -> []
+         [] -> [prev_msg,phases]
        | phase::tl ->
           let msg =
            String.concat "\n\n\n"