FMaps: various updates (mostly suggested by P. Casteran)

- New functions: update (a kind of union), restrict (a kind of inter),
   diff.
- New predicat Partition (and Disjoint), many results about Partition.
- Equivalence instead of obsolete Setoid_Theory (they are aliases).
  refl_st, sym_st, trans_st aren't used anymore and marked as obsolete.
- Start using Morphism (E.eq==>...) instead of compat_...
  This change (FMaps only) is incompatible with 8.2betaX, but it's really
  better now.

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

1 files changed, 11 insertions, 11 deletions

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index ce36ade64..886c95aad 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -449,7 +449,7 @@ Definition transpose (f : A -> B -> B) :=
 Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
   forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
 
-Variable st:Setoid_Theory _ eqB.
+Variable st:Equivalence eqB.
 Variable f:A->B->B.
 Variable i:B.
 Variable Comp:compat_op f.
@@ -459,7 +459,7 @@ Lemma fold_right_eqlistA :
    eqB (fold_right f i s) (fold_right f i s').
 Proof.
 induction 1; simpl; auto.
-refl_st.
+reflexivity.
 Qed.
 
 Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> 
@@ -598,8 +598,8 @@ Lemma fold_right_commutes_restr :
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
 induction s1; simpl; auto; intros.
-refl_st.
-trans_st (f a (f x (fold_right f i (s1++s2)))).
+reflexivity.
+transitivity (f a (f x (fold_right f i (s1++s2)))).
 apply Comp; auto.
 apply IHs1.
 inversion_clear H; auto.
@@ -615,7 +615,7 @@ Lemma fold_right_equivlistA_restr :
 Proof.
  simple induction s.
  destruct s'; simpl.
- intros; refl_st; auto.
+ intros; reflexivity.
  unfold equivlistA; intros.
  destruct (H2 a).
  assert (X : InA a nil); auto; inversion X.
@@ -624,16 +624,16 @@ Proof.
   rewrite <- (E x); auto.
  destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
  subst s'.
- trans_st (f x (fold_right f i (s1++s2))).
+ transitivity (f x (fold_right f i (s1++s2))).
  apply Comp; auto.
  apply Hrec; auto.
  inversion_clear N; auto.
  eapply NoDupA_split; eauto.
  inversion_clear F; auto.
  eapply equivlistA_NoDupA_split; eauto.
- trans_st (f y (fold_right f i (s1++s2))).
- apply Comp; auto; refl_st.
- sym_st; apply fold_right_commutes_restr.
+ transitivity (f y (fold_right f i (s1++s2))).
+ apply Comp; auto. reflexivity.
+ symmetry; apply fold_right_commutes_restr.
  apply ForallList2_equivlistA with (x::l); auto.
 Qed.
 
@@ -654,8 +654,8 @@ Lemma fold_right_commutes : forall s1 s2 x,
   eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
 Proof.
 induction s1; simpl; auto; intros.
-refl_st.
-trans_st (f a (f x (fold_right f i (s1++s2)))).
+reflexivity.
+transitivity (f a (f x (fold_right f i (s1++s2)))); auto.
 Qed.
 
 Lemma fold_right_equivlistA :