diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-06 13:51:55 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-06 13:51:55 -0700 |
| commit | be1f55f6fc260aa42305b40f3853c56883d34550 (patch) | |
| tree | a88e6a3bd53d07548476b8fc08b4f43ad131d231 /src/Util/Notations.v | |
| parent | 89bdd2380c37f07aa5394fd11e1c0b2ca4308790 (diff) | |
Improve some reserved notations
Compatibility with theories/Numbers/NatInt/NZBits.v
Diffstat (limited to 'src/Util/Notations.v')
| -rw-r--r-- | src/Util/Notations.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v index c3f776766..3e0acdcc5 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -16,8 +16,7 @@ Reserved Notation "x ^ 2" (at level 30, format "x ^ 2"). Reserved Notation "x ^ 3" (at level 30, format "x ^ 3"). Reserved Infix "mod" (at level 40, no associativity). Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50). -Reserved Infix "<<" (at level 50). -Reserved Infix "&" (at level 50). -Reserved Infix "<<" (at level 50). +Reserved Infix "<<" (at level 30). +Reserved Infix ">>" (at level 30). Reserved Infix "&" (at level 50). Reserved Infix "~=" (at level 70). |