From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 19 Jun 2006 13:03:33 +0000 (+0000)
Subject: added (but not yet used) remove_local_context
X-Git-Tag: make_still_working~7163
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc8187a8276f45fdf0882acbb832089a10e0d8ed;p=helm.git

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 8b67ddb05..a25ba8e2d 100644
--- 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 5e3f61e1a..c64eacfd6 100644
--- 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