Rewrite

Ltac2.Rewrite

module Strategy : sig ... end

Module for rewrite strategies used by Rewrite.rewrite_strat.

val rewrite_strat : ?in_hyp:ident -> Strategy.t -> unit Proofview.tactic

Runs rewrite strategy on the type of a hypothesis or the goal if in_hyp is None.

• since 9.1