- let stamp = Unix.gettimeofday () in
- let proofterm = NCicProof.mk_proof bag i l in
- prerr_endline (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))); *)