[simpl_map]: avoid using [rewrite .. by ..]
We've been using a patched version of [simpl_map] in our project for a while, with the changes included here.
The core issue is that it seems that [rewrite .. by ..] is not available when explicitly importing ssreflect.
The patch uses by tac
instead, which is in line with what [simplify_map_eq] does later in the file.
I tried to write a quick test to demonstrate the issue; however it seems that triggering it is a bit subtle (while it does definitely occur on our development, I wasn't able to easily reproduce it on my synthetic example--- I think there is some interaction with the exact order of the Require Import invocations).
If deemed necessary I could try harder and try to minimize a problematic instance from our development.
Edited by Robbert Krebbers