New functorialization: paramod is abstracted over a Orderings.Blob, that is like...

[helm.git] / helm / software / components / ng_paramodulation / foUtils.ml

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 10c96f543578f2133898f2077323f85cc1483855..7b57e5bb3d2037b98ff681521c3b55d1ecd6a2cc 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -21,9 +21,9 @@ let rec lexicograph f l1 l2 =
   | _,[] -> 1
 ;;
   
-module Utils (B : Terms.Blob) = struct
-        module Subst = FoSubst;; (*.Subst(B) ;;*)
-  module Order = Orderings.Orderings(B) ;;
+module Utils (B : Orderings.Blob) = struct
+  module Subst = FoSubst;; 
+  module Order = B;;
 
   let rec eq_foterm x y =
     x == y ||