diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-31 18:28:17 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-31 18:28:17 -0700 |
| commit | 2f49243bea4e2c45e2dc433c319754b0105ebd3c (patch) | |
| tree | d3f3f8633cb48e2f6a841f3dd659d864f694a200 /src/Util/Notations.v | |
| parent | 1864e03c51ffc3b39f02c7e32e1e230a8c75e8ba (diff) | |
Add more reserved infixes
Diffstat (limited to 'src/Util/Notations.v')
| -rw-r--r-- | src/Util/Notations.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 8795da399..950005104 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -36,6 +36,16 @@ Reserved Infix "≡_r" (at level 70, no associativity). Reserved Infix "≢_r" (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 "≢₆₄" (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 "≢₅₁₂" (at level 70, no associativity). Reserved Notation "a !== b" (at level 70, no associativity). Reserved Notation "a ≢ b" (at level 70, no associativity). Reserved Notation "$$ v" (at level 40). |