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 bac3e01e004630f5629f021cc6f521dee66d0c42..cf1c0de4df94a203ac73c6ea0ab04be63e8c0642 100644 (file)
--- 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