First implementation of unification on foterms

[helm.git] / helm / software / components / ng_paramodulation / founif.mli

diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli
index d959fc3099e4dd6e82a8ceac58d3c80ae0b450f9..2e801831363e9e96423ade35ebfd5c7da4ffba00 100644 (file)
--- a/helm/software/components/ng_paramodulation/founif.mli
+++ b/helm/software/components/ng_paramodulation/founif.mli
@@ -11,6 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+exception UnificationFailure of string Lazy.t;;
+
 val unification: 
   Terms.varlist -> (* global varlist for both terms t1 and t2 *)
   Terms.varlist -> (* locked variables: if equal to FV(t2) we match t1 with t2*)