debug pps removed

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index b80bfc5001f12aa41b0d9a5d2dfde04be9aee7ad..5f75fb3aa8b24b828a554455df0e0e04fbd4aa02 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -192,11 +192,11 @@ let nparamod rdb metasenv subst context t table =
         let gsteps = List.rev gsteps in
         esteps@(i::gsteps)
       in
-      prerr_endline "YES!";
-      prerr_endline ("Meeting point : " ^ (string_of_int i));
+(*
       prerr_endline "Proof:"; 
       List.iter (fun x -> prerr_endline (string_of_int x);
               prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
+*)
       let proofterm = B.mk_proof bag i l in
       let metasenv, proofterm = 
         let rec aux k metasenv = function
@@ -209,15 +209,11 @@ let nparamod rdb metasenv subst context t table =
         in
          aux 0 metasenv proofterm
       in
-      prerr_endline
-        ("prova generata: " ^ NCicPp.ppterm 
-           ~metasenv ~subst ~context proofterm);
       let metasenv, subst, proofterm, _prooftype = 
         NCicRefiner.typeof 
           (rdb#set_coerc_db NCicCoercion.empty_db) 
           metasenv subst context proofterm None
       in
-      prerr_endline "prova raffinata";
       proofterm, metasenv, subst
   | Failure _ -> prerr_endline "FAILURE"; assert false
 ;;