integration with paramodulation

diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac
index a530cae5600dac6546df9c9ef4a9c7b5ebe91a33..678cc23422ec29fc69d298b2aeb3acfb7525c006 100644 (file)
--- a/helm/matita/configure.ac
+++ b/helm/matita/configure.ac
@@ -38,6 +38,7 @@ $FINDLIB_CLEANREQUIRES \
 unix \
 helm-cic_omdoc \
 helm-tactics \
+helm-paramodulation \
 helm-xml \
 "
 FINDLIB_REQUIRES="\

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 _ =

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 8ec8543bdc6a11482f8a49120dd0956c2ee1ae63..b27e115f43f86e27c6dc637196b0331d6c4b7e59 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -23,5 +23,10 @@
  * http://helm.cs.unibo.it/
  *)
 
+
+(* ALB to link paramodulation... *)
+let _ = Saturation.init ()
+
+  
 let _ = MatitacLib.main `COMPILER