From 932763c609e3a8e32ef4d888a6987a71f0d29825 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Jun 2006 16:49:29 +0000 Subject: [PATCH] the old compute_eq_weight is back (no more max) --- helm/software/components/tactics/paramodulation/utils.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml index a25ba8e2d..542c2dd77 100644 --- a/helm/software/components/tactics/paramodulation/utils.ml +++ b/helm/software/components/tactics/paramodulation/utils.ml @@ -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 -- 2.39.2