2: is_identity -> is_weak_identity

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index b52e074fd1f5317e096322e43b9e46bd6f3ae0cd..625beb839834c27a21b0b5bc17aec3a01afa3629 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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