(* Note: this code is almost identical to change_tac and
* it could be unified by making the change function a callback *)
let reduction_tac ~reduction ~pattern (proof,goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
| _ as t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [metano]
+ (curi,metasenv',_subst,pbo,pty, attrs), [metano]
;;
let simpl_tac ~pattern =
term(s) to be replaced. *)
let change_tac ~pattern with_what =
let change_tac ~pattern ~with_what (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
| _ as t -> t)
metasenv
in
- (curi,metasenv',pbo,pty, attrs), [metano]
+ (curi,metasenv',_subst,pbo,pty, attrs), [metano]
in
mk_tactic (change_tac ~pattern ~with_what)