let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic
- (PrimitiveTactics.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
(Cic.Appl [ _not; ineq]))
status))
|_ -> assert false)
in
let r = apply_tactic
- (PrimitiveTactics.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
w1) status
in