From 0094b2aa93feda2329fdec0131cffc9ea9114f41 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 5 Jul 2016 15:22:03 -0700 Subject: 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 .option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5. --- theories/FSets/FMapFacts.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'theories/FSets') 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. -- cgit v1.2.3 From 2d449a9db34d1cfaff3b698cfc5b435e00100461 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 5 Jul 2016 16:01:04 -0700 Subject: Move option_map notation up This way, it's not eaten by a section --- theories/FSets/FMapFacts.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/FSets') diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 741ee69d3..67bb56448 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. -- cgit v1.2.3