let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) = apply_tactic
- (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ())
+ (EqualityTactics.rewrite_simpl_tac
+ ~direction:`LeftToRight
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ (C.Meta (fresh_meta,irl)))
((curi,metasenv',pbo,pty),goal)
in
let new_goals = fresh_meta::goals in