integrate suggestions by B. Baydemir (see #1930)

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

1 files changed, 25 insertions, 1 deletions

diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index fe6623c33..82c684634 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -509,7 +509,14 @@ the above form:
             | J : _ |- _ => progress (change T with E.t in J)
             | |- _ => progress (change T with E.t)
             end )
-        end).
+        | H : forall x : ?T, _ |- _ =>
+          progress (change T with E.t in H);
+          repeat (
+            match goal with
+            | J : _ |- _ => progress (change T with E.t in J)
+            | |- _ => progress (change T with E.t)
+            end )
+       end).
 
     (** These two tactics take us from Coq's built-in equality
         to [E.eq] (and vice versa) when possible. *)
@@ -747,6 +754,12 @@ the above form:
       In x (singleton x).
     Proof. fsetdec. Qed.
 
+    Lemma test_add_In : forall x y s,
+      In x (add y s) ->
+      ~ E.eq x y ->
+      In x s.
+    Proof. fsetdec. Qed.
+
     Lemma test_Subset_add_remove : forall x s,
       s [<=] (add x (remove x s)).
     Proof. fsetdec. Qed.
@@ -825,6 +838,17 @@ the above form:
       intros until 3. intros g_eq. rewrite <- g_eq. fsetdec.
     Qed.
 
+    Lemma test_baydemir :
+      forall (f : t -> t),
+      forall (s : t),
+      forall (x y : elt),
+      In x (add y (f s)) ->
+      ~ E.eq x y ->
+      In x (f s).
+    Proof.
+      fsetdec.
+    Qed.
+
   End FSetDecideTestCases.
 
 End WDecide.