diff options
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrderedType.v | 2 | ||||
| -rw-r--r-- | theories/Structures/Orders.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index b9510342c..cc8c2261b 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -49,7 +49,7 @@ Module Type OrderedType. Include MiniOrderedType. (** A [eq_dec] can be deduced from [compare] below. But adding this - redundant field allows to see an OrderedType as a DecidableType. *) + redundant field allows seeing an OrderedType as a DecidableType. *) Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }. End OrderedType. 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 *) |