(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false
) context selected_context ([], metasenv, ugraph) in
- let metasenv' =
- List.map (function
- | (n,_,_) when n = metano -> (metano,context',ty')
- | _ as t -> t
- ) metasenv
- in
+ let metasenv' =
+ List.map
+ (function
+ | (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t)
+ metasenv
+ in
(curi,metasenv',pbo,pty), [metano]
in
mk_tactic (change_tac ~pattern ~with_what)