From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 22 Mar 2006 13:47:39 +0000 (+0000)
Subject: :
X-Git-Tag: 0.4.95@7852~1574
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad4b678b155e33fc9bf7264a18f7d60a9fc62ec0;p=helm.git

:
This line, and those below, will be ignored--

M    tactics/paramodulation/utils.ml
---

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index babf684bf..8fb1d42bc 100644
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -292,6 +292,29 @@ end
 
 module IntSet = Set.Make(OrderedInt)
 
+let compute_equality_weight (ty,left,right,o) =
+  let factor = 1 in
+  match o with
+    | Lt -> 
+	let w, m = (weight_of_term 
+	       ~consider_metas:true ~count_metas_occurrences:false right) in
+	  w + (factor * (List.length m)) ;
+    | Le -> assert false
+    | Gt -> 
+	let w, m = (weight_of_term 
+	       ~consider_metas:true ~count_metas_occurrences:false left) in
+	  w + (factor * (List.length m)) ;
+  | Ge -> assert false
+  | Eq 
+  | Incomparable -> 
+      let w1, m1 = (weight_of_term 
+	       ~consider_metas:true ~count_metas_occurrences:false right) in
+      let w2, m2 = (weight_of_term 
+	       ~consider_metas:true ~count_metas_occurrences:false left) in
+      w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
+;;
+
+(* old
 let compute_equality_weight (ty,left,right,o) =
   let metasw = ref 0 in
   let weight_of t =
@@ -306,7 +329,7 @@ let compute_equality_weight (ty,left,right,o) =
   (* let w = weight_of (Cic.Appl [ty;left;right]) in *)
   w + !metasw
 ;;
-
+*)
 
 (* returns a "normalized" version of the polynomial weight wl (with type
  * weight list), i.e. a list sorted ascending by meta number,