* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open ProofEngineTypes
(* Note: this code is almost identical to change_tac and
(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)