diff options
Diffstat (limited to 'theories/Classes/RelationClasses.v')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index f95894be..e1de9ee9 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -13,12 +13,12 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: RelationClasses.v 11800 2009-01-18 18:34:15Z msozeau $ *) +(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. -Require Export Coq.Relations.Relation_Definitions. +Require Import Coq.Relations.Relation_Definitions. (** We allow to unfold the [relation] definition while doing morphism search. *) @@ -368,7 +368,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q We give an equivalent definition, up-to an equivalence relation on the carrier. *) -Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := +Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). (** The equivalence proof is sufficient for proving that [R] must be a morphism @@ -377,7 +377,8 @@ Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R. Proof with auto. - reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. + reduce_goal. + pose proof partial_order_equivalence as poe. do 3 red in poe. apply <- poe. firstorder. Qed. |