Removed debug printing raising Failure

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 73e9809d3ae2d0569761aaac9b00d90bffcdeeae..ec098a61597142d0b603674c27d8cac95487dca4 100644 (file)
--- 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
 ;;