aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Relations
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-06 18:17:24 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-06 18:17:24 +0000
commit53ed1ee05a7c3ceb3b09e2807381af4d961d642b (patch)
tree8d1d246dd1cfebf21472352aa6e5a8c61bfbca01 /theories/Relations
parent6ce9f50c6f516696236fa36e5ff190142496798f (diff)
Plug the new setoid implemtation in, leaving the original one commented
out. The semantics of the old setoid are faithfully simulated by the new tactic, hence no scripts involving rewrite are modified. However, parametric morphism declarations need to be changed, but there are only a few in the standard library, notably in FSets. The declaration and the introduction of variables in the script need to be tweaked a bit, otherwise the proofs remain unchanged. Some fragile scripts not introducting their variable names explicitely were broken. Requiring Setoid requires Program.Basics which sets stronger implicit arguments on some constants, a few scripts benefit from that. Ring/field have been ported but do not really use the new typeclass architecture as well as they could. Performance should be mostly unchanged, but will certainly improve in the near future. Size of the vo's seems not to have changed at all. It will certainly break some contribs using Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Relations')
-rw-r--r--theories/Relations/Relation_Operators.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 8d76b4f4e..61b70ba68 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -83,9 +83,9 @@ Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.
Inductive le_AsB : A + B -> A + B -> Prop :=
- | le_aa : forall x y:A, leA x y -> le_AsB (inl B x) (inl B y)
- | le_ab : forall (x:A) (y:B), le_AsB (inl B x) (inr A y)
- | le_bb : forall x y:B, leB x y -> le_AsB (inr A x) (inr A y).
+ | le_aa : forall x y:A, leA x y -> le_AsB (inl x) (inl y)
+ | le_ab : forall (x:A) (y:B), le_AsB (inl x) (inr y)
+ | le_bb : forall x y:B, leB x y -> le_AsB (inr x) (inr y).
End Disjoint_Union.