X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=a52109e46ad475e526eb9d46d63c74945d5f80a9;hb=04dc7b17e463fa9c75ac91e1df88bf37ed009914;hp=5df1d7d6f243222f4a7cedcaf57b726f8bf6db06;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 5df1d7d6f..a52109e46 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -711,7 +711,7 @@ let activate_theorem (active, passive) =
 ;;
 
 
-
+(*
 let simplify_theorems bag env theorems ?passive (active_list, active_table) =
   let pl, passive_table =
     match passive with
@@ -741,7 +741,7 @@ let simplify_theorems bag env theorems ?passive (active_list, active_table) =
       let p_theorems = List.map (mapfun passive_table) p_theorems in
       List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
 ;;
-
+*)
 
 let rec simpl bag eq_uri env e others others_simpl =
   let active = others @ others_simpl in