let subst,metasenv,ugraph,terms_ty =
match ty with
None -> subst,metasenv,ugraph,None
| Some ty ->
let subst,metasenv,ugraph,res =
select_in_term ~metasenv ~context ~ugraph ~term:ty
let subst,metasenv,ugraph,terms_ty =
match ty with
None -> subst,metasenv,ugraph,None
| Some ty ->
let subst,metasenv,ugraph,res =
select_in_term ~metasenv ~context ~ugraph ~term:ty