From e4158685ac9f6a89c0e208d7c3c0faed84ae45fc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 19 Jun 2006 14:44:11 +0000 Subject: [PATCH] demodulation of goal activated again. 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 | 3 --- 1 file changed, 3 deletions(-) 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> 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 -- 2.39.2