is it possible/feasible to use the SSReflect rewrite
tactic in a standalone fashion, e.g., by aliasing it to ssr_rewrite
and mixing with the regular rewrite
? If not directly, could one do it with some OCaml hacking?
FTR you can always access vanilla rewrite by using rewrite -> ....
and rewrite <- ...
.
sure, but what I'm thinking of is the inverse scenario, we have a project that's "regular ltac", but we think the ssr rewrite
might work better for us.
I guess one would need some OCaml hacking then.
Last updated: Nov 29 2023 at 18:01 UTC