made several occurrences of (eapply ...; eauto) not rely on the lack of pattern unification

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12202 85f007b7-540e-0410-9357-904b9bb8a0f7

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.