From fad8bab9ac50d935f7bf6dd8b940f5c8836b8b77 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 25 Jul 2018 10:01:26 -0400 Subject: Reserve ;;;, fix level of prefix # to not clash with infix # --- src/Util/Notations.v | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/Util/Notations.v b/src/Util/Notations.v index ae9a34533..c010534a5 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -90,6 +90,7 @@ Reserved Notation "A <--- X ; B" (at level 70, X at next level, right associativ Reserved Notation "A <---- X ; B" (at level 70, X at next level, right associativity, format "'[v' A <---- X ; '/' B ']'"). Reserved Notation "A <----- X ; B" (at level 70, X at next level, right associativity, format "'[v' A <----- X ; '/' B ']'"). Reserved Notation "A ;; B" (at level 70, right associativity, format "'[v' A ;; '/' B ']'"). +Reserved Notation "A ;;; B" (at level 70, right associativity, format "'[v' A ;;; '/' B ']'"). Reserved Notation "u [ i ]" (at level 30). Reserved Notation "v [[ i ]]" (at level 30). Reserved Notation "u {{ i }}" (at level 30). @@ -140,7 +141,13 @@ Reserved Notation "A ~> R" (at level 99). Reserved Notation "A --->" (left associativity, at level 65). Reserved Notation "'return' x" (at level 70, format "'return' x"). Reserved Notation "f x" (only printing, at level 10, left associativity). -Reserved Notation "# x" (at level 0, format "# x"). -Reserved Notation "## x" (at level 0, format "## x"). -Reserved Notation "### x" (at level 0, format "### x"). +(* 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 .. 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