From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Sep 2006 17:08:10 +0000 (+0000)
Subject: 2: is_identity -> is_weak_identity
X-Git-Tag: 0.4.95@7852~965
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d6973b9a2130071e96f1260be78e30d709b2180;p=helm.git

2: is_identity -> is_weak_identity
---

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b52e074fd..625beb839 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -438,7 +438,6 @@ let check_for_deep_subsumption env active_table eq =
 
 (** simplifies current using active and passive *)
 let forward_simplify bag eq_uri env current (active_list, active_table) =
-  prerr_endline (Equality.string_of_equality ~env current);
   let _, context, _ = env in
   let demodulate table current = 
     let newmeta, newcurrent =
@@ -490,7 +489,7 @@ let forward_simplify_new bag eq_uri env new_pos active =
   let new_pos_set =
     List.fold_left
       (fun s e ->
-         if not (Equality.is_identity env e) then
+         if not (Equality.is_weak_identity e) then
            EqualitySet.add e s
          else s)
       EqualitySet.empty new_pos
@@ -565,7 +564,7 @@ let backward_simplify_active
       active_list (([],pruned), Indexing.empty),
     List.fold_right
       (fun eq p ->
-         if (Equality.is_identity env eq) then p
+         if (Equality.is_weak_identity eq) then p
          else eq::p)
       newa []
   in
@@ -748,7 +747,6 @@ let rec simpl bag eq_uri env e others others_simpl =
       Indexing.empty active
   in
   let res = 
-    if Equality.is_weak_identity e then None else 
       forward_simplify bag eq_uri env e (active, tbl) 
   in
     match others with
@@ -1140,7 +1138,7 @@ let rec saturate_equations bag eq_uri env goal accept_fun passive active =
                              (Equality.string_of_equality ~env current)));
         let new' = infer bag eq_uri env current active in
         let active =
-          if Equality.is_identity env current then active
+          if Equality.is_weak_identity (*env*) current then active
           else
             let al, tbl = active in
             al @ [current], Indexing.index tbl current