Code restructuring.

[helm.git] / helm / ocaml / tactics / paramodulation / inference.mli

diff --git a/helm/ocaml/tactics/paramodulation/inference.mli b/helm/ocaml/tactics/paramodulation/inference.mli
index fde29e3527685bfe49a7265ec4c98303f590ffa5..b31d8bacff7dc10b2f69eb5427f53498afdae7fa 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/inference.mli
+++ b/helm/ocaml/tactics/paramodulation/inference.mli
@@ -123,6 +123,7 @@ val meta_convertibility: Cic.term -> Cic.term -> bool
 (** meta convertibility between two equations *)
 val meta_convertibility_eq: equality -> equality -> bool
 
+val is_weak_identity: environment -> equality -> bool
 val is_identity: environment -> equality -> bool
 
 val string_of_equality: ?env:environment -> equality -> string