]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: errors of phase 7 were no longer printed :-)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Dec 2005 16:01:46 +0000 (16:01 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Dec 2005 16:01:46 +0000 (16:01 +0000)
helm/matita/matitaExcPp.ml

index 29f08d514980cdfea95218be2f06a7ebf400a1c3..af1aeb882964661d01e722ef905fc3d681c2e545 100644 (file)
@@ -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"