let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic
- (PrimitiveTactics.change_tac ~what:ty
+ (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
~with_what:(Cic.Appl [ _not; ineq]))
status))
~continuation:(Tacticals.then_
|_ -> assert false)
in
let r = apply_tactic
- (PrimitiveTactics.change_tac ~what:ty ~with_what:w1)
- status in
+ (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
+ ~with_what:w1) status in
debug("fine MY_CHNGE\n");
r))
~continuation:(*PORTINGTacticals.id_tac*)tac2]))