diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-25 11:48:05 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-25 11:48:05 -0700 |
| commit | bf0d9280ebf806eef8ee3280f7976edb3282ae6e (patch) | |
| tree | b7a6e171a03a1912c480da38d1d961e7324f92f3 /src/Util/Notations.v | |
| parent | 34d53cc72df1a3c31838e0cc7e06f0cf8959d628 (diff) | |
Integrate suggestions from Andres
Diffstat (limited to 'src/Util/Notations.v')
| -rw-r--r-- | src/Util/Notations.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 686443829..8795da399 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -27,6 +27,7 @@ Reserved Infix "~=" (at level 70). Reserved Infix "==" (at level 70, no associativity). Reserved Infix "=~>" (at level 70, no associativity). Reserved Infix "<~=" (at level 70, no associativity). +Reserved Infix "<~=~>" (at level 70, no associativity). Reserved Infix "≡" (at level 70, no associativity). Reserved Infix "≢" (at level 70, no associativity). Reserved Infix "≡_n" (at level 70, no associativity). |