ProofEngineTypes.apply_tactic
(EqualityTactics.rewrite_tac ~direction:`RightToLeft
~pattern:(ProofEngineTypes.conclusion_pattern None)
- (Cic.Meta(newmeta,irl)))
+ (Cic.Meta(newmeta,irl)) [])
(proof'',goal)
in
let goal = match goals with [g] -> g | _ -> assert false in