From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 4 Mar 2010 07:55:14 +0000 (+0000)
Subject: Small changes for debugging
X-Git-Tag: make_still_working~3016
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=754f74638de5c287c849dc72494143b1da82cd88;p=helm.git

Small changes for debugging
---

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 0558e89c7..8abdaaec5 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -12,8 +12,8 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 let print s = prerr_endline (Lazy.force s) ;; 
-(* let debug = print *) 
-let debug s = ();; 
+let noprint s = ();;  
+let debug = noprint;;
 
 let monster = 100;;
     
@@ -346,12 +346,12 @@ module Paramod (B : Orderings.Blob) = struct
 		  (Unix.gettimeofday())));
     let actives_l, active_t = actives in
     let passive_t,wset,_ = passives in
-    let _ = debug
+    let _ = noprint
       (lazy 
 	 ("Actives :" ^ (String.concat ";\n" 
 	    (List.map Pp.pp_unit_clause actives_l)))) in 
     let wset = IDX.elems passive_t in
-    let _ = debug
+    let _ = noprint
       (lazy 
 	 ("Passives:" ^(String.concat ";\n" 
 	    (List.map (fun _,cl -> Pp.pp_unit_clause cl)
@@ -452,7 +452,7 @@ module Paramod (B : Orderings.Blob) = struct
       Sup.simplify_goal 
         ~no_demod maxvar (snd actives) bag g_actives current 
     with
-      | None -> status
+      | None -> debug (lazy "None"); status
       | Some (bag,g_current) -> 
 	  let _ = 
 	    debug (lazy("Infer on goal : "