From fae6f153d6dad76b6ccfce17a6b3d997db338d2e Mon Sep 17 00:00:00 2001
From: Enrico Zoli <??>
Date: Fri, 20 Oct 2006 08:35:00 +0000
Subject: [PATCH] Serious bug fixed: without a Lazy.force the user obtained an
 error comparing two functional values.

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

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index bac3e01e0..cf1c0de4d 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -187,7 +187,10 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn
      "equal" element. I.e. we are showing the error corresponding to the
      most advanced disambiguation pass *)
   let choices =
-   let choices_compare (_,e1,_,_,m1) (_,e2,_,_,m2) = compare (e1,m1) (e2,m2) in
+   let choices_compare (_,e1,_,_,m1) (_,e2,_,_,m2) =
+    let m1 = Lazy.force m1 in
+    let m2 = Lazy.force m2 in
+     compare (e1,m1) (e2,m2) in
    let choices_compare_by_passes (p1,_,_,_,_) (p2,_,_,_,_) = compare p1 p2 in
    let rec uniq =
     function
-- 
2.39.2