fixed LetIn proofs

[helm.git] / components / tactics / paramodulation / saturation.ml

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b5b727b4d42d55554dc05e70969ba667f500e205..445eccdbc2f217565c67b5f319cb2652c105066e 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1771,6 +1771,7 @@ let saturate
         let initial = newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
+prerr_endline (CicPp.pp goal_proof names);
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let side_effects_t = 
         List.map (Subst.apply_subst subsumption_subst) side_effects_t