X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=84a3cf9f5236daaee3b0a91274745127486a9c3d;hb=38c54dd8e2234836d5f3e8011c478daf7d59fa25;hp=7c66cc40bced62d6e3a889a38164627513a41064;hpb=8a3045a162622e8a76ffdb267309faff496ee7ec;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index 7c66cc40b..84a3cf9f5 100644
--- 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