From: Enrico Zoli <??>
Date: Fri, 20 Oct 2006 08:35:00 +0000 (+0000)
Subject: Serious bug fixed: without a Lazy.force the user obtained an error comparing
X-Git-Tag: 0.4.95@7852~874
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fae6f153d6dad76b6ccfce17a6b3d997db338d2e;p=helm.git

Serious bug fixed: without a Lazy.force the user obtained an error comparing
two functional values.
---

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