- let stamp = Unix.gettimeofday () in
- let proofterm = NCicProof.mk_proof bag i fo_subst l in
- print (lazy (Printf.sprintf "Got proof term in %fs"
- (Unix.gettimeofday() -. stamp)));
+ (* let stamp = Unix.gettimeofday () in *)
+ let proofterm,prooftype = NCicProof.mk_proof bag i fo_subst l in
+ (* debug (lazy (Printf.sprintf "Got proof term in %fs"
+ (Unix.gettimeofday() -. stamp))); *)