(Some (_, C.Decl t)) when
fst (R.are_convertible context (S.lift n t) ty
CicUniv.empty_ugraph) -> n
- | (Some (_, C.Def (_,Some ty'))) when
+ | (Some (_, C.Def (_,ty'))) when
fst (R.are_convertible context (S.lift n ty') ty
CicUniv.empty_ugraph) -> n
- | (Some (_, C.Def (t,None))) ->
- let ty_t, u = (* TASSI: FIXME *)
- CicTypeChecker.type_of_aux' metasenv context (S.lift n t)
- CicUniv.empty_ugraph in
- let b,_ = R.are_convertible context ty_t ty u in
- if b then n else find (n+1) tl
| _ -> find (n+1) tl
)
| [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))