added some code to print the praamodulation proofs with a graph

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

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 30561bf07b5df933fecb0da1e3efef1be1539207..ff58512ea9d1f47c429d6f0f6b412fc5c96b4165 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1343,6 +1343,7 @@ let build_proof
         eq_uri goalproof initial type_of_goal side_effects
         context proof_menv  
   in
+(*   Equality.draw_proof bag names goalproof newproof subsumption_id; *)
   let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
   let real_menv =  fix_metasenv (proof_menv@metasenv) in
   let real_menv,goal_proof =