Small changes for debugging

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 0558e89c7432309155c4f07ead3c8dc794b8d88e..8abdaaec509301e7ef7cae20300601925d9739f0 100644 (file)
--- 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 : "