;;
let look_for_coercion src tgt =
+ None
+ (*
if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
(tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con"))
then
(CicPp.ppterm tgt));
None
end
+ *)
;;
(cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
;;
+let type_of_aux' metasenv context term ugraph =
+ try
+ type_of_aux' metasenv context term ugraph
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+
+
(* DEBUGGING ONLY
let type_of_aux' metasenv context term =
try