Added more precise time information

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 8530be3e8b571b14c01ef6d65e28ed1c5a172091..4968d3290030c7e1b47441bf79d2b9242006db7f 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,7 +1,7 @@
 (* LOOPING : COL057-1.ma *)
 
 let debug s =
-  prerr_endline s
+  () (* prerr_endline s *)
 ;;
 
 let nparamod rdb metasenv subst context t table =
@@ -182,12 +182,15 @@ let nparamod rdb metasenv subst context t table =
        let gsteps,esteps = traverse true ([],[]) i in
          (List.rev esteps)@gsteps
       in
-       prerr_endline (Printf.sprintf "Found proof in %d iterations" !nb_iter);
+       prerr_endline (Printf.sprintf "Found proof in %d iterations, %fs"
+                        !nb_iter
+                        (Unix.gettimeofday() -. timeout +. amount_of_time));
       (* prerr_endline "Proof:"; 
       List.iter (fun x -> prerr_endline (string_of_int x);
               prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;*)
       let proofterm = B.mk_proof bag i l in
-       prerr_endline "Got proof term";
+       prerr_endline (Printf.sprintf "Got proof term, %fs"
+                        (Unix.gettimeofday() -. timeout +. amount_of_time));
       let metasenv, proofterm = 
         let rec aux k metasenv = function
           | NCic.Meta _ as t -> metasenv, t