integration with paramodulation

[helm.git] / helm / matita / matita.ml

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 0a3f72d4d37d97e6424eb3535147886527b3aef5..0b5919ab9e8b28f78c7a81035eb2615ebdb7fcbf 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -29,6 +29,11 @@ open MatitaGtkMisc
 open MatitaTypes
 open MatitaMisc
 
+
+(* ALB to link paramodulation... *)
+let _ = Saturation.init ()
+  
+
 (** {2 Initialization} *)
 
 let _ =