added (but not yet used) remove_local_context

weight of non oriented equations decreased

diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index 8b67ddb05a6a0b05ecee68300a69d29a142e9295..a25ba8e2d7cda49cb9ac8cfede5cb14ea2aef99d 100644 (file)
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/components/tactics/paramodulation/utils.ml
@@ -103,6 +103,13 @@ let metas_of_term term =
   aux term
 ;;
 
+let rec remove_local_context =
+  function
+    | Cic.Meta (i,_) -> Cic.Meta (i,[])
+    | Cic.Appl l ->
+       Cic.Appl(List.map remove_local_context l)
+    | t -> t 
+
 
 (************************* rpo ********************************)
 let number = [
@@ -311,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
-      w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
+      (max w1 w2)+(max (factor * (List.length m1)) (factor * (List.length m2)))
 ;;
 
 (* old

diff --git a/helm/software/components/tactics/paramodulation/utils.mli b/helm/software/components/tactics/paramodulation/utils.mli
index 5e3f61e1a409e9ab5acc6f1fb4717059ccf172f4..c64eacfd61f3c3364df483305e51624d04e96aab 100644 (file)
--- a/helm/software/components/tactics/paramodulation/utils.mli
+++ b/helm/software/components/tactics/paramodulation/utils.mli
@@ -88,3 +88,5 @@ val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int
 val debug_print: string Lazy.t -> unit
 
 val metas_of_term: Cic.term -> int list
+
+val remove_local_context: Cic.term -> Cic.term