From: Enrico Tassi Date: Thu, 1 Jun 2006 13:28:19 +0000 (+0000) Subject: fix X-Git-Tag: 0.4.95@7852~1365 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9de7ac55904a21812fbf1da5dacc7722c489362e;p=helm.git fix --- diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index e4dec6397..9c5ea281b 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -181,8 +181,17 @@ let check_target context target msg = let get_candidates ?env mode tree term = let s = match mode with - | Matching -> Index.retrieve_generalizations tree term - | Unification -> Index.retrieve_unifiables tree term + | Matching -> + let _ = <:start> in + <:stop> + | Unification -> + let _ = <:start> in + <:stop> + in Index.PosEqSet.elements s ;; diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 2b3bcc069..a26ec0f73 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1223,7 +1223,8 @@ let simplify_goal_set env goals passive active = (fun acc goal -> match simplify_goal env goal ~passive active with | _, g -> if find g acc then acc else g::acc) - active_goals active_goals + (* active_goals active_goals *) + [] active_goals in if List.length active_goals <> List.length simplified then prerr_endline "SEMPLIFICANDO HO SCARTATO..."; @@ -1305,7 +1306,9 @@ let given_clause (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 @@ -1376,7 +1379,10 @@ let given_clause prerr_endline "simpl goal with new"; let goals = let a,b,_ = build_table new' in + let _ = <:start> in + <:stop> in let passive = add_to_passive passive new' in step goals theorems passive active (iterno+1)