aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sets/Partial_Order.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sets/Partial_Order.v')
-rwxr-xr-xtheories/Sets/Partial_Order.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 5ef6bc9b0..15fc690dd 100755
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -48,7 +48,7 @@ Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y.
Inductive covers (y x:U) : Prop :=
Definition_of_covers :
Strict_Rel_of x y ->
- ~ ( exists z : _ | Strict_Rel_of x z /\ Strict_Rel_of z y) ->
+ ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) ->
covers y x.
End Partial_orders.