fix

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index e4dec639749adff715b48e7ce993d7d4ca45296c..9c5ea281b9fbc65509f36488cfdd98597b279bc0 100644 (file)
--- 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<retrieve_generalizations>> in
+        <:stop<retrieve_generalizations
+        Index.retrieve_generalizations tree term
+        >>
+    | Unification -> 
+        let _ = <:start<retrieve_unifiables>> in
+        <:stop<retrieve_unifiables
+        Index.retrieve_unifiables tree term
+        >>
+        
   in
   Index.PosEqSet.elements s
 ;;

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index 2b3bcc0692d5d44d007d6e063747cc0bfbdb5fb2..a26ec0f73b40c5d9c4ae552655735b56919e7a8c 100644 (file)
--- 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<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 
@@ -1376,7 +1379,10 @@ let given_clause
                   prerr_endline "simpl goal with new";
                   let goals = 
                     let a,b,_ = build_table new' in
+                    let _ = <:start<simplify_goal_set new>> in
+                    <:stop<simplify_goal_set new
                     simplify_goal_set env goals passive (a,b)
+                    >>
                   in
                   let passive = add_to_passive passive new' in
                   step goals theorems passive active (iterno+1)