From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 19 Jun 2006 14:44:11 +0000 (+0000)
Subject: demodulation of goal activated again.
X-Git-Tag: make_still_working~7160
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e4158685ac9f6a89c0e208d7c3c0faed84ae45fc;p=helm.git

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 67a328275..050ab49eb 100644
--- 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