let gty = NCicUntrusted.apply_subst subst ctx gty in
let build_status (pt, _, metasenv, subst) =
try
- print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+ debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
let stamp = Unix.gettimeofday () in
let metasenv, subst, pt, pty =
(* NCicRefiner.typeof status
let status,t = term_of_cic_term status t ctx in
let _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof subst metasenv ctx t in
- print(lazy("prima"));
let ty,metasenv,args =
match gty with
| NCic.Const(nref)
| NCic.Appl l -> NCic.Appl(l@args)
| _ -> NCic.Appl(t::args)
in
- print(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
- print(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
+ noprint(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
+ noprint(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
let eq_coerc =
let uri =
NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in