context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context ^
- "\nReason: " ^ Printexc.to_string exn))) exn
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Printexc.to_string exn*)))) exn
(* }}} end coercion stuff *)
in
eat_prods_and_args pristinemenv metasenv subst context pristinehe he