From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 1 Sep 2005 08:42:30 +0000 (+0000)
Subject: Comment added.
X-Git-Tag: working_equations_only~2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=308684ed4a405d37dcca6a7f38a404c6967e2e0e;p=helm.git

Comment added.
---

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 525ed9ca2..c1c9086de 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -107,6 +107,8 @@ let compute_equality_weight ty left right =
 (*     metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *)
     w
   in
+  (* Warning: the following let cannot be expanded since it forces the
+     right evaluation order!!!! *)
   let w = (weight_of ty) + (weight_of left) + (weight_of right) in
   w + !metasw
 (*     (4 * IntSet.cardinal !metasw) *)