diff options
Diffstat (limited to 'theories/FSets/FMapFacts.v')
| -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. |