- 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

2 files changed, 3 insertions, 3 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 6d77a6a0c..617ea6f4f 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -651,7 +651,7 @@ Proof. unfold Equal; congruence. Qed.
 
 Definition Equal_ST : forall elt:Type, Setoid_Theory (t elt) (@Equal _).
 Proof. 
-constructor; [apply Equal_refl | apply Equal_sym | apply Equal_trans].
+constructor; red; [apply Equal_refl | apply Equal_sym | apply Equal_trans].
 Qed.
 
 Add Relation key E.eq 
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 0c19176f8..6afb8fcb7 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -295,12 +295,12 @@ End BoolSpec.
 
 Definition E_ST : Setoid_Theory elt E.eq.
 Proof.
-constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
+constructor ; red; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
 Qed.
 
 Definition Equal_ST : Setoid_Theory t Equal.
 Proof. 
-constructor; [apply eq_refl | apply eq_sym | apply eq_trans].
+constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans].
 Qed.
 
 Add Relation elt E.eq