New version of deep_subsumption

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

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index 2d7e48e5cb13dd18ba66d6f0f7543622630b26e3..1a2a3a2808d3d284a4f00f4eda4ebe289f5b2ca5 100644 (file)
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -46,7 +46,7 @@ and old_proof =
 
 and goal_proof = (Utils.pos * int * substitution * Cic.term) list
 
-val pp_proof: (Cic.name option) list -> goal_proof -> string
+val pp_proof: (Cic.name option) list -> goal_proof -> new_proof -> string
 
 val empty_subst : substitution
 val apply_subst : substitution -> Cic.term -> Cic.term