From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Dec 2005 16:01:46 +0000 (+0000)
Subject: Bug fixed: errors of phase 7 were no longer printed :-)
X-Git-Tag: make_still_working~8029
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c5ffc85f9cac2ccf3176c72683f1d2c411c3951;hp=cd8062bb6dbbc4564c4d35e3bc1557b030568902;p=helm.git

Bug fixed: errors of phase 7 were no longer printed :-)
---

diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml
index 29f08d514..af1aeb882 100644
--- a/helm/matita/matitaExcPp.ml
+++ b/helm/matita/matitaExcPp.ml
@@ -66,7 +66,7 @@ let rec to_string =
   | MatitaDisambiguator.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"