X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2FnCicBlob.mli;fp=matitaB%2Fcomponents%2Fng_paramodulation%2FnCicBlob.mli;h=6adb2042160029ece1462c6a50ef9dd2ec7fcb81;hb=97e59118f8cc0d98c51c0d41e8e7704344666cdb;hp=5d0c7ae2ba0e5fad112522aa0ca3f6f1bffe864a;hpb=85d772f5c3d5c86bbb474ba7ab4a259dc06687f9;p=helm.git

diff --git a/matitaB/components/ng_paramodulation/nCicBlob.mli b/matitaB/components/ng_paramodulation/nCicBlob.mli
index 5d0c7ae2b..6adb20421 100644
--- a/matitaB/components/ng_paramodulation/nCicBlob.mli
+++ b/matitaB/components/ng_paramodulation/nCicBlob.mli
@@ -13,14 +13,21 @@
 
 val set_eqP: NCic.term -> unit
 val set_default_eqP: unit -> unit
+val saturate: 
+    #NCicEnvironment.status ->
+    NCic.metasenv ->
+    NCic.substitution ->
+    NCic.context -> NCic.term -> NCic.term -> NCic.term * NCic.term
 
+(*
 module type NCicContext = 
   sig
     val metasenv : NCic.metasenv
     val subst : NCic.substitution
     val context : NCic.context
   end
+*)
 
-module NCicBlob(C : NCicContext) : Terms.Blob 
+module NCicBlob: Terms.Blob 
 with type t = NCic.term and type input = NCic.term