sig type dir = [ `Left | `Right ] val tactical : TacRewrite.dir -> Tactical.tactical val strategy : ?priority:float -> TacRewrite.dir -> Tactical.selection -> Strategy.strategy end