The discriminate tactic accepts a term, not only an identifier!

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

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 1adf90e5045094c048c30fe624f3d4ade8b2e068..71f2fc1b5d5a3adee6f1d2634784b2c3797bb9f1 100644 (file)
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -31,3 +31,11 @@ val lpo: Cic.term -> Cic.term -> comparison
 
 (** term-ordering function settable by the user *)
 val compare_terms: (Cic.term -> Cic.term -> comparison) ref
+
+type equality_sign = Negative | Positive
+
+val string_of_sign: equality_sign -> string
+
+type pos = Left | Right 
+
+val string_of_pos: pos -> string