From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- theories/FSets/FMapFacts.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'theories/FSets/FMapFacts.v') 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. -- cgit v1.2.3