The Blob is not abstracted on the context any more.

[helm.git] / matitaB / components / ng_paramodulation / nCicBlob.mli

diff --git a/matitaB/components/ng_paramodulation/nCicBlob.mli b/matitaB/components/ng_paramodulation/nCicBlob.mli
index 5d0c7ae2ba0e5fad112522aa0ca3f6f1bffe864a..6adb2042160029ece1462c6a50ef9dd2ec7fcb81 100644 (file)
--- 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