- begin
- prerr_endline (
- (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
- (Printf.sprintf "\ntall: %.9f" tall) ^
- (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
- (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
- (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
- (Printf.sprintf "\nbeta_expand_time: %.9f\n"
- !Indexing.beta_expand_time) ^
- (Printf.sprintf "\nmetas_of_proof: %.9f\n"
- !Inference.metas_of_proof_time) ^
- (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
- (Printf.sprintf "\nforward_simpl_new_times: %.9f"
- !forward_simpl_new_time) ^
- (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
- (Printf.sprintf "\npassive_maintainance_time: %.9f"
- !passive_maintainance_time))
- end;
+ begin
+ prerr_endline (
+ (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
+ (Printf.sprintf "\ntall: %.9f" tall) ^
+ (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
+ (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
+ (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
+ (Printf.sprintf "\nbeta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "\nmetas_of_proof: %.9f\n"
+ !Inference.metas_of_proof_time) ^
+ (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
+ (Printf.sprintf "\nforward_simpl_new_times: %.9f"
+ !forward_simpl_new_time) ^
+ (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
+ (Printf.sprintf "\npassive_maintainance_time: %.9f"
+ !passive_maintainance_time))
+ end;