From fc3f8eb9bcb6645a97a35335d588dbd50231689b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 8 Apr 2008 16:15:23 +0000
Subject: - 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
---
 theories/FSets/FMapFacts.v | 2 +-
 theories/FSets/FSetFacts.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/FSets')

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 6d77a6a0cc..617ea6f4f6 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 0c19176f82..6afb8fcb7b 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 
-- 
cgit v1.2.3