Duplication du fichier FSetProperties pour les ensembles Weak.

Du coup, factorisation d'une partie dans SetoidList. Ajout de 
lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface 
concernant elements. 



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

1 files changed, 23 insertions, 0 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 3bf86eb48..9496099a8 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -662,3 +662,26 @@ Implicit Arguments Setoid_Theory [].
 Implicit Arguments Seq_refl [].
 Implicit Arguments Seq_sym [].
 Implicit Arguments Seq_trans [].
+
+
+(* Some tactics for manipulating Setoid Theory not officially 
+   declared as Setoid. *)
+
+Ltac trans_st x := match goal with 
+  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+     apply (Seq_trans _ _ H) with x; auto
+ end.
+
+Ltac sym_st := match goal with 
+  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+     apply (Seq_sym _ _ H); auto
+ end.
+
+Ltac refl_st := match goal with 
+  | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => 
+     apply (Seq_refl _ _ H); auto
+ end.
+
+Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
+Proof. constructor; congruence. Qed.
+