diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 437f52ab0..bf10728c8 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1793,7 +1793,7 @@ Lemma map2_2 : forall m m' y, bst m -> bst m' -> In y (map2 f m m') -> In y m \/ In y m'. Proof. unfold map2; intros. -eapply map2_opt_2 with (f0:=fun _ => f); eauto; intros. +eapply map2_opt_2 with (f0:=fun _ => f); try eassumption; trivial; intros. apply map_option_bst; auto. apply map_option_bst; auto. rewrite map_option_find; auto. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 6db4077f1..6a062ea14 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -954,11 +954,13 @@ Module OrdProperties (M:S). elements s = elements_lt x s ++ elements_ge x s. Proof. unfold elements_lt, elements_ge, leb; intros. - eapply (@filter_split _ E.eq); eauto with set. ME.order. ME.order. ME.order. + eapply (@filter_split _ E.eq); trivial with set; auto with set. + ME.order. ME.order. ME.order. intros. rewrite gtb_1 in H. assert (~E.lt y x). - unfold gtb in *; destruct (E.compare x y); intuition; try discriminate; ME.order. + unfold gtb in *; destruct (E.compare x y); intuition; + try discriminate; ME.order. ME.order. Qed. |