diff options
Diffstat (limited to 'theories/Classes/CRelationClasses.v')
| -rw-r--r-- | theories/Classes/CRelationClasses.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index c014ecc7ab..2dd254496b 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -337,7 +337,7 @@ Section Binary. morphism for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) - Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R. + Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R. Proof with auto. reduce_goal. apply H. firstorder. |