X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsubst.ml;h=b8cadf48cda2955969009f8fe0bfe8735db12212;hb=b60b04a930b208dc0bf8876305c4fa5ea2aeb619;hp=662a9f0d71c8e4d067c8e77c7dbdce7a29e913d6;hpb=46bfce7d0f09058ca063766192a1d4251ce7df63;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/subst.ml b/helm/software/components/ng_paramodulation/subst.ml
index 662a9f0d7..b8cadf48c 100644
--- a/helm/software/components/ng_paramodulation/subst.ml
+++ b/helm/software/components/ng_paramodulation/subst.ml
@@ -9,26 +9,30 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-let empty_subst = [];;
-
-let buildsubst n t tail = (n,t) :: tail ;;
-
-let rec lookup_subst var subst =
-  match var with
-    | Terms.Var i ->
-        (try
-          lookup_subst (List.assoc i subst) subst
-        with
-            Not_found -> var)
-    | _ -> var
-;;
-
-let is_in_subst i subst = List.mem_assoc i subst;;
-
-(* filter out from metasenv the variables in substs *)
-let filter subst varlist =
-  List.filter
-    (fun m ->
-       not (is_in_subst m subst))
-    varlist
-;;
+module Subst (B : Terms.Blob) = struct
+  
+  let empty_subst = [];;
+  
+  let buildsubst n t tail = (n,t) :: tail ;;
+  
+  let rec lookup_subst var subst =
+    match var with
+      | Terms.Var i ->
+          (try
+            lookup_subst (List.assoc i subst) subst
+          with
+              Not_found -> var)
+      | _ -> var
+  ;;
+  
+  let is_in_subst i subst = List.mem_assoc i subst;;
+  
+  (* filter out from metasenv the variables in substs *)
+  let filter subst varlist =
+    List.filter
+      (fun m ->
+         not (is_in_subst m subst))
+      varlist
+  ;;
+  
+end