+ | Some (n,Cic.Def (te,ty)) ->
+ (try
+ ignore
+ (CicTypeChecker.type_of_aux' metasenv context te
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *));
+ ignore
+ (CicTypeChecker.type_of_aux' metasenv context ty
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *));
+ with
+ _ ->
+ raise
+ (PET.Fail
+ (lazy ("The correctness of hypothesis " ^
+ string_of_name n ^
+ " relies on the body of " ^ hyp)
+ )));
+ entry::context