]> matita.cs.unibo.it Git - helm.git/commitdiff
demodulation of goal activated again.
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 19 Jun 2006 14:44:11 +0000 (14:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 19 Jun 2006 14:44:11 +0000 (14:44 +0000)
to deactivate it, the check_if_goal_set_us_solved should be moved after the infeer_goal step

helm/software/components/tactics/paramodulation/saturation.ml

index 67a328275b2d68b543ef16d2c079a566a5f8043b..050ab49ebb490525fa01309f749399bce7a67e4c 100644 (file)
@@ -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