aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes')
-rw-r--r--theories/Classes/RelationClasses.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 25316c278..17a645c8f 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -388,7 +388,7 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R.
Proof with auto.
- reduce_goal. pose 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.