X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Ffounif.mli;h=2e801831363e9e96423ade35ebfd5c7da4ffba00;hb=4514417676056e0be6cc481a931e70a627882867;hp=d959fc3099e4dd6e82a8ceac58d3c80ae0b450f9;hpb=46bfce7d0f09058ca063766192a1d4251ce7df63;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli
index d959fc309..2e8018313 100644
--- 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*)