From 308684ed4a405d37dcca6a7f38a404c6967e2e0e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 1 Sep 2005 08:42:30 +0000 Subject: [PATCH] Comment added. --- helm/ocaml/paramodulation/utils.ml | 2 ++ 1 file changed, 2 insertions(+) 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) *) -- 2.39.2