Skip to content
Snippets Groups Projects

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

Closed 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

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading