some optimizations...

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

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 0cc0fcb708d9f51be2a844a04fece6b5656e433a..5ced528bb81055550961d65e489068bded9c49cf 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -79,3 +79,6 @@ val subsumption: environment -> equality -> equality -> bool
 val metas_of_term: Cic.term -> int list
 
 val fix_metas: int -> equality -> int * equality
+
+val extract_differing_subterms:
+  Cic.term -> Cic.term -> (Cic.term * Cic.term) option