diff options
Diffstat (limited to 'theories/Structures/Orders.v')
| -rw-r--r-- | theories/Structures/Orders.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index e179bd8b4..724690b42 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -95,7 +95,7 @@ Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation. (** NB: in [OrderedType], an [eq_dec] could be deduced from [compare]. - But adding this redundant field allows to see an [OrderedType] as a + But adding this redundant field allows seeing an [OrderedType] as a [DecidableType]. *) (** * Versions with [eq] being the usual Leibniz equality of Coq *) |