functorial abstraction over term blobs

[helm.git] / helm / software / components / ng_paramodulation / founif.mli

diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli
index 2e801831363e9e96423ade35ebfd5c7da4ffba00..55f15e65647a8c80468ec43f3682d396adc9497f 100644 (file)
--- a/helm/software/components/ng_paramodulation/founif.mli
+++ b/helm/software/components/ng_paramodulation/founif.mli
@@ -13,12 +13,15 @@
 
 exception UnificationFailure of string Lazy.t;;
 
+module Founif (B : Terms.Blob) : 
+  sig
+
 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
+  B.t Terms.foterm ->
+  B.t Terms.foterm ->
+     B.t Terms.substitution * Terms.varlist
 
 (*
 val unification: 
@@ -30,3 +33,5 @@ val matching:
    'a Terms.substitution * Terms.varlist
 
 *)
+
+  end