diff options
author | Benjamin Barenblat <bbaren@google.com> | 2019-04-26 17:10:05 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@google.com> | 2019-04-26 17:10:05 -0400 |
commit | 6de992d169e076f2e579e14b0d64ff68616e04b0 (patch) | |
tree | 8e9d90a802227b60ed1f4b387ddec8d4084e530d /src/Util | |
parent | 4483d41d6a510e01041f05546643934c9d2a887b (diff) |
Restore `Reserved Notation` directives for `$ x` and `# x`, which were
commented out to avoid conflicts with bbv. Make both notations `at level
9, x at level 9`, which matches unary prefix operators throughout the
rest of the development.
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Notations.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 9549e0ba6..63f529762 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -171,15 +171,10 @@ Reserved Notation "'return' x" (at level 70, format "'return' x"). Reserved Notation "f x" (only printing, at level 10, left associativity). (* TODO: Remove this next one if and when we drop support for Coq 8.7; it's present in the stdlib in 8.8 *) Reserved Notation "{ x & P }" (at level 0, x at level 99). -(* TODO: Uncomment this block when https://github.com/mit-plv/bbv/pull/13 is merged Reserved Notation "$ x" (at level 9, x at level 9, format "$ x"). -Reserved Notation "# x" (at level 55, x at level 9, format "# x"). (* 55, so we don't clash with [_ # _] *) - *) +Reserved Notation "# x" (at level 9, x at level 9, format "# x"). Reserved Notation "## x" (at level 9, x at level 9, format "## x"). Reserved Notation "### x" (at level 9, x at level 9, format "### x"). Reserved Notation "#### x" (at level 9, x at level 9, format "#### x"). Reserved Notation "##### x" (at level 9, x at level 9, format "##### x"). Reserved Notation "\ x .. y , t" (at level 200, x binder, y binder, right associativity, format "\ x .. y , '//' t"). - -(* TODO: Remove these when https://github.com/mit-plv/bbv/pull/13 is merged *) -Reserved Notation "# x" (at level 0, format "# x"). |