diff options
Diffstat (limited to 'theories/Structures/OrderedType.v')
| -rw-r--r-- | theories/Structures/OrderedType.v | 2 |
1 files changed, 1 insertions, 1 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. |