Subsumption_subst must be applied to the initial proof before passing

[helm.git] / components / tactics / paramodulation / equality.mli

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index 8c55516a9db82167e95189458ebe3608649b033a..cd60c5408e649456735932a9cc55c5a69a0ed9ef 100644 (file)
--- a/components/tactics/paramodulation/equality.mli
+++ b/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;;
 
 (**