:

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 babf684bf97ea27a42c4623603960565fee5d4be..8fb1d42bcf60bf6adae07c5ae7826995632f245e 100644 (file)
--- 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,