diff options
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrderedType2.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v index 5b669db4e0..1cddfea3b1 100644 --- a/theories/Structures/OrderedType2.v +++ b/theories/Structures/OrderedType2.v @@ -32,11 +32,13 @@ Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe. Module Type LtNotation (E:EqLt). Infix "<" := E.lt. + Notation "x > y" := (y<x) (only parsing). Notation "x < y < z" := (x<y /\ y<z). End LtNotation. Module Type LeNotation (E:EqLe). Infix "<=" := E.le. + Notation "x >= y" := (y<=x) (only parsing). Notation "x <= y <= z" := (x<=y /\ y<=z). End LeNotation. |