]> matita.cs.unibo.it Git - helm.git/commitdiff
the old compute_eq_weight is back (no more max)
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 27 Jun 2006 16:49:29 +0000 (16:49 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 27 Jun 2006 16:49:29 +0000 (16:49 +0000)
helm/software/components/tactics/paramodulation/utils.ml

index a25ba8e2d7cda49cb9ac8cfede5cb14ea2aef99d..542c2dd77d26e6c6bae42937abd63d9fc2257a72 100644 (file)
@@ -318,7 +318,7 @@ let compute_equality_weight (ty,left,right,o) =
               ~consider_metas:true ~count_metas_occurrences:false right) in
       let w2, m2 = (weight_of_term 
               ~consider_metas:true ~count_metas_occurrences:false left) in
-      (max w1 w2)+(max (factor * (List.length m1)) (factor * (List.length m2)))
+      w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
 ;;
 
 (* old