From ff6a35c50aace7c20d4f68a1ac4a0d751cfc72e3 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 31 Oct 2006 09:03:15 +0000
Subject: [PATCH] New behaviour of the disambiguation error messages: errors
 generated without using coercions are shown only when More is pressed.

---
 matita/matitaGui.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 998cdc339..c718bd81a 100644
--- a/matita/matitaGui.ml
+++ b/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
-- 
2.39.2