From e5014674aed0dab6f3aa43773c8caeffcfe0ac32 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 21 Jul 2005 11:53:48 +0000 Subject: [PATCH] integration with paramodulation --- helm/matita/configure.ac | 1 + helm/matita/matita.ml | 5 +++++ helm/matita/matitac.ml | 5 +++++ 3 files changed, 11 insertions(+) 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 -- 2.39.2