diff options
Diffstat (limited to 'theories/FSets/FMapFacts.v')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index eaeb2914..3c5690a7 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. @@ -1986,7 +1988,7 @@ Module OrdProperties (M:S). simpl; intros; try discriminate. intros. destruct a; destruct l; simpl in *. - injection H; clear H; intros; subst. + injection H as -> ->. inversion_clear H1. red in H; simpl in *; intuition. elim H0; eauto. @@ -2050,10 +2052,10 @@ Module OrdProperties (M:S). generalize (elements_3 m). destruct (elements m). try discriminate. - destruct p; injection H; intros; subst. - inversion_clear H1. + destruct p; injection H as -> ->; intros H4. + inversion_clear H1 as [? ? H2|? ? H2]. red in H2; destruct H2; simpl in *; ME.order. - inversion_clear H4. + inversion_clear H4. rename H1 into H3. rewrite (@InfA_alt _ eqke) in H3; eauto with *. apply (H3 (y,x0)); auto. Qed. |