removed some debug messages

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index c964e3a78c882f525df690c230ec60e18abd1eb4..1d2d6a9048a12361851620fdf7bd461e47755ac9 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -363,11 +363,11 @@ let subsumption env table target =
       in
        ok left rightr
   in
-    (if r then 
-       debug_print 
-        (lazy
-           (Printf.sprintf "SUBSUMPTION! %s\n%s\n"
-              (Inference.string_of_equality target) (Utils.print_subst s))));
+(*     (if r then  *)
+(*        debug_print  *)
+(*      (lazy *)
+(*         (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
+(*            (Inference.string_of_equality target) (Utils.print_subst s)))); *)
     r, s
 ;;
 
@@ -505,8 +505,8 @@ let rec demodulation_equality newmeta env table sign target =
           incr maxmeta;
           let irl =
             CicMkImplicit.identity_relocation_list_for_metavariable context in
-          debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
-          print_newline ();
+(*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
+(*           print_newline (); *)
           C.Meta (!maxmeta, irl)
         in
           let eq_found =
@@ -593,13 +593,13 @@ let rec demodulation_equality newmeta env table sign target =
     if !Utils.compare_terms left' left = Utils.Lt then left' else left in
   let newright = 
     if !Utils.compare_terms right' right = Utils.Lt then right' else right in
-  if newleft != left || newright != right then (
-    debug_print
-      (lazy
-        (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n"
-           (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right)
-           (CicPp.ppterm right')))
-  );
+(*   if newleft != left || newright != right then ( *)
+(*     debug_print *)
+(*       (lazy *)
+(*      (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *)
+(*         (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *)
+(*         (CicPp.ppterm right'))) *)
+(*   ); *)
   let w' = Utils.compute_equality_weight ty newleft newright in
   let o' = !Utils.compare_terms newleft newright in
   newmeta, (w', p, (ty, newleft, newright, o'), m, a)
@@ -753,7 +753,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
   let maxmeta = ref newmeta in
   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 
-    debug_print (lazy "\nSUPERPOSITION LEFT\n");
+(*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
 
     let time1 = Unix.gettimeofday () in
     
@@ -795,10 +795,10 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
         in
         match proof with
         | Inference.BasicProof _ ->
-            debug_print (lazy "replacing a BasicProof");
+(*             debug_print (lazy "replacing a BasicProof"); *)
             pb
         | Inference.ProofGoalBlock (_, parent_proof) ->
-            debug_print (lazy "replacing another ProofGoalBlock");
+(*             debug_print (lazy "replacing another ProofGoalBlock"); *)
             Inference.ProofGoalBlock (pb, parent_proof)
         | _ -> assert false
       in
@@ -943,7 +943,7 @@ let rec demodulation_goal newmeta env table goal =
         incr maxmeta;
         let irl =
           CicMkImplicit.identity_relocation_list_for_metavariable context in
-        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
+(*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
         C.Meta (!maxmeta, irl)
       in
       let eq_found =
@@ -966,19 +966,19 @@ let rec demodulation_goal newmeta env table goal =
         in
         let rec repl = function
           | Inference.NoProof ->
-              debug_print (lazy "replacing a NoProof");
+(*               debug_print (lazy "replacing a NoProof"); *)
               pb
           | Inference.BasicProof _ ->
-              debug_print (lazy "replacing a BasicProof");
+(*               debug_print (lazy "replacing a BasicProof"); *)
               pb
           | Inference.ProofGoalBlock (_, parent_proof) ->
-              debug_print (lazy "replacing another ProofGoalBlock");
+(*               debug_print (lazy "replacing another ProofGoalBlock"); *)
               Inference.ProofGoalBlock (pb, parent_proof)
           | (Inference.SubProof (term, meta_index, p) as subproof) ->
-              debug_print
-                (lazy
-                   (Printf.sprintf "replacing %s"
-                      (Inference.string_of_proof subproof)));
+(*               debug_print *)
+(*                 (lazy *)
+(*                    (Printf.sprintf "replacing %s" *)
+(*                       (Inference.string_of_proof subproof))); *)
               Inference.SubProof (term, meta_index, repl p)
           | _ -> assert false
         in repl proof