X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.mli;h=d52483ddb08a8b5705f5ee9c733c106fef65976d;hb=f7aedf0ebd0fb55d3587db4f0753521927dcbb69;hp=9704c45ec0a39c4b74d7629dc839ce85e70fa812;hpb=b6bec181b81b3cbc56ec8914dcd7e6a029c7d84f;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 9704c45ec..d52483ddb 100644
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -56,9 +56,13 @@ val lpo: Cic.term -> Cic.term -> comparison
 
 val kbo: Cic.term -> Cic.term -> comparison
 
+val ao: Cic.term -> Cic.term -> comparison
+
 (** term-ordering function settable by the user *)
 val compare_terms: (Cic.term -> Cic.term -> comparison) ref
 
+val guarded_simpl:  Cic.context -> Cic.term -> Cic.term
+
 type equality_sign = Negative | Positive
 
 val string_of_sign: equality_sign -> string