Skip to content

[simpl_map]: avoid using [rewrite .. by ..]

Armaël Guéneau requested to merge Armael/stdpp:simpl_map into master

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

Merge request reports