From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 21 Jul 2005 11:53:48 +0000 (+0000)
Subject: integration with paramodulation
X-Git-Tag: V_0_7_2~127
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e5014674aed0dab6f3aa43773c8caeffcfe0ac32;p=helm.git

integration with paramodulation
---

diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac
index a530cae56..678cc2342 100644
--- 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 0a3f72d4d..0b5919ab9 100644
--- 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 8ec8543bd..b27e115f4 100644
--- 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