From: Enrico Tassi Date: Mon, 19 Jun 2006 14:44:11 +0000 (+0000) Subject: demodulation of goal activated again. X-Git-Tag: 0.4.95@7852~1294 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=126e56fc8eb4096f8c133258e5d43f82305ebd0b;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/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 67a328275..050ab49eb 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/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> in let goals = simplify_goal_set env goals passive active in let _ = <:stop> 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