From 0d6973b9a2130071e96f1260be78e30d709b2180 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 17:08:10 +0000 Subject: [PATCH] 2: is_identity -> is_weak_identity --- components/tactics/paramodulation/saturation.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) 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 -- 2.39.2