let find_pattern_for name =
try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
with Not_found -> None in
let subst,metasenv,ugraph,ty_terms =
select_in_term ~metasenv ~context ~ugraph ~term:ty
~pattern:(what,goal_pattern) in
let find_pattern_for name =
try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
with Not_found -> None in
let subst,metasenv,ugraph,ty_terms =
select_in_term ~metasenv ~context ~ugraph ~term:ty
~pattern:(what,goal_pattern) in