functorial abstraction over term blobs

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

diff --git a/helm/software/components/ng_paramodulation/subst.mli b/helm/software/components/ng_paramodulation/subst.mli
index 73f5115ddacecfe6a0c4184da498925eeef1f5a2..8747a478fa49e8817b118ebed326d3503e7e62d6 100644 (file)
--- a/helm/software/components/ng_paramodulation/subst.mli
+++ b/helm/software/components/ng_paramodulation/subst.mli
@@ -11,8 +11,13 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val empty_subst : 'a Terms.substitution
-val buildsubst : 
-  int -> 'a Terms.foterm -> 'a Terms.substitution -> 'a Terms.substitution
-val lookup_subst : 'a Terms.foterm -> 'a Terms.substitution -> 'a Terms.foterm
-val filter : 'a Terms.substitution -> Terms.varlist -> Terms.varlist
+module Subst (B : Terms.Blob) : 
+  sig
+    val empty_subst : B.t Terms.substitution
+    val buildsubst : 
+      int -> B.t Terms.foterm -> B.t Terms.substitution -> 
+       B.t Terms.substitution
+    val lookup_subst : 
+          B.t Terms.foterm -> B.t Terms.substitution -> B.t Terms.foterm
+    val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist
+  end