X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.mli;h=cd60c5408e649456735932a9cc55c5a69a0ed9ef;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=8c55516a9db82167e95189458ebe3608649b033a;hpb=0e6ba9d1134a3bfe9fd4d5b4495faf0811a216df;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index 8c55516a9..cd60c5408 100644
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -70,6 +70,7 @@ val refl_proof: Cic.term -> Cic.term -> Cic.term
 val fix_metas: int -> equality -> int * equality
 val metas_of_proof: proof -> int list
 
+val add_subst : Subst.substitution -> proof -> proof
 exception TermIsNotAnEquality;;
 
 (**