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

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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 1a588043409a66b5f40b07014885accfe653b4a1..f86d4d36e77bd0bf67b0319a795e7bc0f5a0b52f 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -11,12 +11,12 @@
 
 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
 
-module Superposition (B : Terms.Blob) = 
+module Superposition (B : Orderings.Blob) = 
   struct
     module IDX = Index.Index(B)
     module Unif = FoUnif.Founif(B)
     module Subst = FoSubst 
-    module Order = Orderings.Orderings(B)
+    module Order = B
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)