From: Enrico Tassi <enrico.tassi@inria.fr>
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<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 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<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)