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