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: make_still_working~6733
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=9e0bf389e79dbc38e917c527489453dcf5a15983;p=helm.git

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index bac3e01e0..cf1c0de4d 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/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