(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false
) context selected_context ([], metasenv, ugraph) in
(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false
) context selected_context ([], metasenv, ugraph) in