* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open ProofEngineTypes
(* Note: this code is almost identical to change_tac and
let pairs, metasenv, ugraph =
List.fold_left
(fun (pairs, metasenv, ugraph) (context_of_t, t) ->
-prerr_endline "++++++++++++++++++++++++++";
-prerr_endline "context_of_t";
-prerr_endline (CicMetaSubst.ppcontext [] context_of_t);
-prerr_endline "t";
-prerr_endline (CicMetaSubst.ppterm [] t);
let with_what, metasenv, ugraph =
with_what context_of_t metasenv ugraph
in
(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)