Discrimination and trie removed.

[helm.git] / helm / ocaml / paramodulation / utils.mli

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 9704c45ec0a39c4b74d7629dc839ce85e70fa812..d52483ddb08a8b5705f5ee9c733c106fef65976d 100644 (file)
--- 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