From 339418b59ec90edbe16980e2978a0e8be347aa1e Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 22 Jun 2009 15:39:28 +0000
Subject: 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
---
 theories/FSets/FMapAVL.v        | 2 +-
 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 437f52ab08..bf10728c8e 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 6db4077f1e..6a062ea14a 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.
 
-- 
cgit v1.2.3