- A little cleanup in Classes/*. Separate standard morphisms on

relf/sym/trans relations from morphisms on prop connectives and
relations.
- Add general order theory on predicates, instantiated for relations.
Derives equivalence, implication, conjunction and disjunction as
liftings from propositional connectives. Can be used for n-ary
homogeneous predicates thanks to a bit of metaprogramming with lists of
types. 
- Rebind Setoid_Theory to use the Equivalence record type instead of
declaring an isomorphic one. One needs to do "red" after constructor to
get the same statements when building objects of type Setoid_Theory, so
scripts break.


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

1 files changed, 8 insertions, 12 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 983c651ab..8f59c048f 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -8,22 +8,18 @@
 
 (*i $Id$: i*)
 
-Set Implicit Arguments.
-
 Require Export Coq.Classes.SetoidTactics.
 
 (** For backward compatibility *)
 
-Record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop := 
-  { Seq_refl : forall x:A, Aeq x x;
-    Seq_sym : forall x y:A, Aeq x y -> Aeq y x;
-    Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z }.
-
-Implicit Arguments Setoid_Theory [].
-Implicit Arguments Seq_refl [].
-Implicit Arguments Seq_sym [].
-Implicit Arguments Seq_trans [].
-
+Definition Setoid_Theory := @Equivalence.  
+Definition Build_Setoid_Theory := @Build_Equivalence.  
+Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x :=
+  Eval compute in reflexivity.
+Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x :=
+  Eval compute in symmetry.
+Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z :=
+  Eval compute in transitivity.
 
 (** Some tactics for manipulating Setoid Theory not officially 
     declared as Setoid. *)