(match hd with
(Some (_, C.Decl t)) when
(R.are_convertible context (S.lift n t) ty) -> n
- | (Some (_, C.Def t)) when
+ | (Some (_, C.Def (_,Some ty'))) when
+ (R.are_convertible context ty' ty) -> n
+ | (Some (_, C.Def (t,None))) when
(R.are_convertible context
(CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
| _ -> find (n+1) tl