From 6de992d169e076f2e579e14b0d64ff68616e04b0 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Fri, 26 Apr 2019 17:10:05 -0400 Subject: Clean up notations after bbv removal 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. --- src/Util/Notations.v | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'src/Util') 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"). -- cgit v1.2.3