diff options
| author | Jason Gross | 2016-07-05 16:01:04 -0700 |
|---|---|---|
| committer | GitHub | 2016-07-05 16:01:04 -0700 |
| commit | 2d449a9db34d1cfaff3b698cfc5b435e00100461 (patch) | |
| tree | 5be4b49a6c46f5c6d4c5788adc4fe4c69f28f290 | |
| parent | 0094b2aa93feda2329fdec0131cffc9ea9114f41 (diff) | |
Move option_map notation up
This way, it's not eaten by a section
| -rw-r--r-- | theories/FSets/FMapFacts.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 741ee69d31..67bb56448b 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -24,6 +24,8 @@ Hint Extern 1 (Equivalence _) => constructor; congruence. Module WFacts_fun (E:DecidableType)(Import M:WSfun E). +Notation option_map := option_map (compat "8.4"). + Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. @@ -437,8 +439,6 @@ 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. |