- | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
- | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
+ | Some (_,C.Def (_,Some ty)) -> S.lift n ty
+ | Some (_,C.Def (bo,None)) ->
+ prerr_endline "##### CASO DA INVESTIGARE E CAPIRE" ;
+ type_of_aux context (S.lift n bo)
+ | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)