let termty =
CicSubstitution.subst_vars exp_named_subst_diff termty
in
- prerr_endline ("term:" ^ CicPp.ppterm term);
- prerr_endline ("termty:" ^ CicPp.ppterm termty);
+(* prerr_endline ("term:" ^ CicPp.ppterm term);*)
+(* prerr_endline ("termty:" ^ CicPp.ppterm termty);*)
let subst,newmetasenv',t =
try
new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty