restored is_identity instead of is_weak_identity

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index ff5bf23cbbaae16548a4dd6a643fa089856ec96c..12c8e9bd65c6eb3a7ea6eadb2dd916db6b5e2494 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -843,7 +843,7 @@ let superposition_right bag
   in
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
-  let ok e = not (Equality.is_weak_identity (*metasenv', context, ugraph*) e) in
+  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 8e53df28f23e62f9352e2d299633c67f4dd5fedd..b5026d32079bcb435d6301da675e9f9b9969234a 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -120,7 +120,7 @@ let make_passive eq_list =
   let set =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
   in
-  (*EqualitySet.elements set*) List.rev eq_list, set (* see applys.ma *)
+  (*EqualitySet.elements set*) eq_list, set (* see applys.ma *)
 ;;
 let make_empty_active () = [], Indexing.empty ;;
 let make_active eq_list = 
@@ -444,7 +444,7 @@ let forward_simplify bag eq_uri env current (active_list, active_table) =
       Indexing.demodulation_equality bag eq_uri !maxmeta env table current
     in
     maxmeta := newmeta;
-    if Equality.is_weak_identity newcurrent then None else Some newcurrent
+    if Equality.is_identity env newcurrent then None else Some newcurrent
   in
   let demod current =
     if Utils.debug_metas then
@@ -489,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_weak_identity e) then
+         if not (Equality.is_identity env e) then
            EqualitySet.add e s
          else s)
       EqualitySet.empty new_pos
@@ -556,7 +556,7 @@ let backward_simplify_active
       (fun eq ((res,pruned), tbl) ->
          if List.mem eq res then
            (res, (id_of_eq eq)::pruned),tbl 
-         else if (Equality.is_weak_identity eq) || (find eq res) then (
+         else if (Equality.is_identity env eq) || (find eq res) then (
            (res, (id_of_eq eq)::pruned),tbl
          ) 
          else
@@ -564,7 +564,7 @@ let backward_simplify_active
       active_list (([],pruned), Indexing.empty),
     List.fold_right
       (fun eq p ->
-         if (Equality.is_weak_identity eq) then p
+         if (Equality.is_identity env eq) then p
          else eq::p)
       newa []
   in
@@ -743,7 +743,7 @@ let rec simpl bag eq_uri env e others others_simpl =
   let tbl =
     List.fold_left
       (fun t e -> 
-         if Equality.is_weak_identity e then t else Indexing.index t e) 
+         if Equality.is_identity env e then t else Indexing.index t e) 
       Indexing.empty active
   in
   let res = 
@@ -1138,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_weak_identity (*env*) current then active
+          if Equality.is_identity env current then active
           else
             let al, tbl = active in
             al @ [current], Indexing.index tbl current