diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-07-05 15:22:03 -0700 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-07-05 15:22:03 -0700 |
| commit | 0094b2aa93feda2329fdec0131cffc9ea9114f41 (patch) | |
| tree | 81a60837f6cc373b6267b8a810925f2f59881ad2 /theories/FSets | |
| parent | 2df88d833767f6a43ac8f08627e1cb9cc0c8b30d (diff) | |
Restore option_map in FMapFacts
This definition was removed by a4043608f704f026de7eb5167a109ca48e00c221 (This commit adds full universe polymorphism and fast projections to Coq), for reasons I do not know. This means that things like `unfold option_map` work only in 8.5, while `unfold <application of Facts>.option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5.
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index eaeb2914b..741ee69d3 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -437,6 +437,8 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. destruct (eq_dec x y); auto. Qed. +Notation option_map := option_map (compat "8.4"). + Lemma map_o : forall m x (f:elt->elt'), find x (map f m) = option_map f (find x m). Proof. |