From: denes <??>
Date: Tue, 23 Jun 2009 17:57:40 +0000 (+0000)
Subject: Removed debug printing raising Failure
X-Git-Tag: make_still_working~3813
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10a9a8c36ff36e6a53bda1ec3074cb2fac03da63;p=helm.git

Removed debug printing raising Failure
---

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 73e9809d3..ec098a615 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -92,8 +92,6 @@ let nparamod rdb metasenv subst context t table =
       Sup.infer_right bag maxvar current actives 
     in
       debug "Demodulating goals with actives...";
-      debug ("Current : " ^ (Pp.pp_unit_clause current));
-      debug ("Active goal : " ^ (Pp.pp_unit_clause (List.hd g_actives)));
       (* keep goals demodulated w.r.t. actives and check if solved *)
       let bag, g_actives = 
 	List.fold_left 
@@ -102,8 +100,6 @@ let nparamod rdb metasenv subst context t table =
 	       bag, c::acc) 
           (bag,[]) g_actives 
       in
-      debug (Pp.pp_unit_clause current);
-      debug (Pp.pp_unit_clause (List.hd g_actives));
       let ctable = IDX.index_unit_clause IDX.DT.empty current in
       let bag, maxvar, new_goals = 
 	List.fold_left 
@@ -117,8 +113,6 @@ let nparamod rdb metasenv subst context t table =
 	PassiveSet.empty new_clauses in
       let new_goals = List.fold_left add_passive_clause
 	PassiveSet.empty new_goals in
-	debug (string_of_int (PassiveSet.cardinal new_goals));
-	debug (string_of_int (PassiveSet.cardinal g_passives));
 	bag, maxvar, actives,
     PassiveSet.union new_clauses passives, g_actives,
     PassiveSet.union new_goals g_passives
@@ -221,7 +215,7 @@ let nparamod rdb metasenv subst context t table =
               let metasenv,i,_,_=NCicMetaSubst.mk_meta metasenv context `Term in
               metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
           | t -> NCicUntrusted.map_term_fold_a 
-                  (fun _ k -> k+1) k aux metasenv t                 
+                  (fun _ k -> k+1) k aux metasenv t
         in
          aux 0 metasenv proofterm
       in
@@ -231,6 +225,8 @@ let nparamod rdb metasenv subst context t table =
           metasenv subst context proofterm None
       in
       proofterm, metasenv, subst
-  | Failure _ -> prerr_endline
+  | Failure s -> 
+      prerr_endline s;
+      prerr_endline
       (Printf.sprintf "FAILURE in %d iterations" !nb_iter); assert false
 ;;