X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fterms.mli;h=02e3a8b6686b865f2975a44747ee4b19369399d5;hb=497563d35f24bbcbcbd8d669d73284b76a823118;hp=f5aaa619f2dc01dfac4c13d661f7cc29b65597bd;hpb=3c1a432c1612f8ed21f5b2220005599c4d9da1d5;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index f5aaa619f..02e3a8b66 100644
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -18,7 +18,7 @@ type 'a foterm =
 
 type 'a substitution = (int * 'a foterm) list
 
-type comparison = Lt | Le | Eq | Ge | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable
 
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 type direction = Left2Right | Right2Left | Nodir