X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Ffounif.mli;h=fc682c5fc102849d4932097f73aa9f0e0d02f52e;hb=b60b04a930b208dc0bf8876305c4fa5ea2aeb619;hp=2e801831363e9e96423ade35ebfd5c7da4ffba00;hpb=4514417676056e0be6cc481a931e70a627882867;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli
index 2e8018313..fc682c5fc 100644
--- a/helm/software/components/ng_paramodulation/founif.mli
+++ b/helm/software/components/ng_paramodulation/founif.mli
@@ -13,20 +13,16 @@
 
 exception UnificationFailure of string Lazy.t;;
 
-val unification: 
-  Terms.varlist -> (* global varlist for both terms t1 and t2 *)
-  Terms.varlist -> (* locked variables: if equal to FV(t2) we match t1 with t2*)
-  'a Terms.foterm ->
-  'a Terms.foterm ->
-     'a Terms.substitution * Terms.varlist
+module Founif (B : Terms.Blob) : 
+  sig
 
-(*
-val unification: 
-  Terms.varlist -> 'a Terms.foterm -> 'a Terms.foterm -> 
-   'a Terms.substitution * Terms.varlist
-
-val matching:
-  Terms.varlist -> Terms.varlist -> 'a Terms.foterm -> 'a Terms.foterm -> 
-   'a Terms.substitution * Terms.varlist
+   val unification: 
+     (* global varlist for both terms t1 and t2 *)
+     Terms.varlist -> 
+     (* locked variables: if equal to FV(t2) we match t1 with t2*)
+     Terms.varlist -> 
+     B.t Terms.foterm ->
+     B.t Terms.foterm ->
+        B.t Terms.substitution * Terms.varlist
 
-*)
+  end