aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Notations.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/Notations.v')
-rw-r--r--src/Util/Notations.v7
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").