type_of_aux subst metasenv context expected_type ugraph1
in
let actual_type = CicReduction.whd ~subst context actual_type in
- prerr_endline (CicPp.ppterm expected_type');
- prerr_endline (CicPp.ppterm actual_type);
let subst,metasenv,ugraph3 =
try
fo_unif_subst subst context metasenv