demodulation of goal activated again.

to deactivate it, the check_if_goal_set_us_solved should be moved after the infeer_goal step

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 67a328275b2d68b543ef16d2c079a566a5f8043b..050ab49ebb490525fa01309f749399bce7a67e4c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1090,12 +1090,10 @@ let given_clause
     else if Unix.gettimeofday () > max_time then
       (ParamodulationFailure "No more time to spend")
     else
-      (* 
       let _ = prerr_endline "simpl goal with active" in
       let _ = <:start<simplify goal set active>> in
       let goals = simplify_goal_set env goals passive active in 
       let _ = <:stop<simplify goal set active>> in
-      *)
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
           prerr_endline 
@@ -1146,7 +1144,6 @@ let given_clause
               | Some current ->
                   (* GENERATION OF NEW EQUATIONS *)
                   prerr_endline "infer";
-                 let _,_,_,_,id = Equality.open_equality current in
                   let new' = infer eq_uri env current active in
                   prerr_endline "infer goal";
                   let goals = infer_goal_set_with_current env current goals in