From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 31 Oct 2006 09:03:15 +0000 (+0000)
Subject: New behaviour of the disambiguation error messages: errors generated without
X-Git-Tag: make_still_working~6691
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84be7b1bb35ea49d9b24f21710a893bb7772f4d5;p=helm.git

New behaviour of the disambiguation error messages: errors generated without
using coercions are shown only when More is pressed.
---

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 998cdc339..c718bd81a 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -236,7 +236,10 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn
  offset errorll
 = 
   let errorll' =
-   if all_passes then errorll else List.rev (List.tl (List.tl (List.rev errorll))) in
+   if all_passes then errorll else
+    (* We remove passes 1,2 and 5,6 *)
+    []::[]::
+     List.tl (List.tl (List.rev (List.tl (List.tl (List.rev errorll))))) in
   let choices =
    let pass = ref 0 in
    List.flatten