let subst,metasenv,ugraph,ty_terms =
select_in_term ~metasenv ~context ~ugraph ~term:ty
~pattern:(what,goal_pattern) in
let subst,metasenv,ugraph,context_terms =
let subst,metasenv,ugraph,res,_ =
(List.fold_right
let subst,metasenv,ugraph,ty_terms =
select_in_term ~metasenv ~context ~ugraph ~term:ty
~pattern:(what,goal_pattern) in
let subst,metasenv,ugraph,context_terms =
let subst,metasenv,ugraph,res,_ =
(List.fold_right