prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
*)
let ty_sort1,u = (*TASSI: FIXME *)
- CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph in
(*
prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
*)