Merge SetoidList2 into SetoidList.

This file contains low-level stuff for FSets/FMaps. Switching it to
the new version (the one using Equivalence and so on instead of
eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in
FSets/FMaps that are minor and probably invisible to standard users.

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

1 files changed, 5 insertions, 4 deletions

diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 796db9f8f..1b1bae352 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -133,7 +133,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
    forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}),
    compat_P E.eq P -> compat_bool E.eq (fdec Pdec).
   Proof.
-    unfold compat_P, compat_bool, fdec in |- *; intros.
+    unfold compat_P, compat_bool, Proper, respectful, fdec in |- *; intros.
     generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
   Qed.
 
@@ -217,7 +217,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     intros s1 s2; simpl in |- *.
     intros; assert (compat_bool E.eq (fdec Pdec)); auto.
     intros; assert (compat_bool E.eq (fun x => negb (fdec Pdec x))).
-    generalize H2; unfold compat_bool in |- *; intuition;
+    generalize H2; unfold compat_bool, Proper, respectful in |- *; intuition;
      apply (f_equal negb); auto.
     intuition.
     generalize H4; unfold For_all, Equal in |- *; intuition.
@@ -662,7 +662,8 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
    forall f : elt -> bool,
    compat_bool E.eq f -> compat_P E.eq (fun x => f x = true).
   Proof.
-     unfold compat_bool, compat_P in |- *; intros; rewrite <- H1; firstorder.
+     unfold compat_bool, compat_P, Proper, respectful, impl; intros;
+      rewrite <- H1; firstorder.
   Qed.
 
   Hint Resolve compat_P_aux.
@@ -768,7 +769,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
     intro p; case p; clear p; intros s1 s2 H C.
     generalize (H (compat_P_aux C)); clear H; intro H.
     assert (D : compat_bool E.eq (fun x => negb (f x))).
-    generalize C; unfold compat_bool in |- *; intros; apply (f_equal negb);
+    generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb);
      auto.
     simpl in |- *; unfold Equal in |- *; intuition.
     apply filter_3; firstorder.