Various architectural changes

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

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index 7c66cc40bced62d6e3a889a38164627513a41064..84a3cf9f5236daaee3b0a91274745127486a9c3d 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -32,10 +32,10 @@ module type Blob =
   end
 
 module NRKBO (B : Terms.Blob) : Blob 
-with type t = B.t and type input = B.input
+with type t = B.t 
 
 module KBO (B : Terms.Blob) : Blob 
-with type t = B.t and type input = B.input
+with type t = B.t 
 
-module LPO (B : Terms.Blob) : Blob 
-with type t = B.t and type input = B.input
+module LPO (B : Terms.Blob) : Blob
+with type t = B.t