Skip to content

Commit

Permalink
Moving at level 10 notations which were originally at level 200.
Browse files Browse the repository at this point in the history
This follows what was done for notations at level binder_constr in Coq
PR #18014.
  • Loading branch information
herbelin authored and JasonGross committed Nov 1, 2023
1 parent 77a2f7d commit 991c3c9
Showing 1 changed file with 13 additions and 13 deletions.
26 changes: 13 additions & 13 deletions src/Util/Notations.v
Original file line number Diff line number Diff line change
Expand Up @@ -115,28 +115,28 @@ Reserved Notation "v [[ i ]]" (at level 30).
Reserved Notation "u {{ i }}" (at level 30).
Reserved Notation "a # b" (at level 55, no associativity). (* match with theories/QArith/QArith_base.v *)
Reserved Notation "'plet' x := y 'in' z"
(at level 200, z at level 200, format "'plet' x := y 'in' '//' z").
(at level 10, z at level 200, format "'plet' x := y 'in' '//' z").
Reserved Notation "'nlet' x := A 'in' b"
(at level 200, b at level 200, x at level 99, format "'nlet' x := A 'in' '//' b").
(at level 10, b at level 200, x at level 99, format "'nlet' x := A 'in' '//' b").
Reserved Notation "'nlet' x : tx := A 'in' b"
(at level 200, b at level 200, x at level 99, format "'nlet' x : tx := A 'in' '//' b").
(at level 10, b at level 200, x at level 99, format "'nlet' x : tx := A 'in' '//' b").
Reserved Notation "'slet' x .. y := A 'in' b"
(at level 200, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b").
(at level 10, x binder, y binder, b at level 200, format "'slet' x .. y := A 'in' '//' b").
Reserved Notation "'llet' x := A 'in' b"
(at level 200, b at level 200, format "'llet' x := A 'in' '//' b").
(at level 10, b at level 200, format "'llet' x := A 'in' '//' b").
Reserved Notation "'expr_let' x := A 'in' b"
(at level 200, b at level 200, format "'expr_let' x := A 'in' '//' b").
(at level 10, b at level 200, format "'expr_let' x := A 'in' '//' b").
Reserved Notation "'mlet' x := A 'in' b"
(at level 200, b at level 200, format "'mlet' x := A 'in' '//' b").
(at level 10, b at level 200, format "'mlet' x := A 'in' '//' b").
(* Note that making [Let] a keyword breaks the vernacular [Let] in Coq 8.4 *)
Reserved Notation "'dlet_nd' x .. y := v 'in' f"
(at level 200, x binder, y binder, f at level 200, format "'dlet_nd' x .. y := v 'in' '//' f").
(at level 10, x binder, y binder, f at level 200, format "'dlet_nd' x .. y := v 'in' '//' f").
Reserved Notation "'dlet' x .. y := v 'in' f"
(at level 200, x binder, y binder, f at level 200, format "'dlet' x .. y := v 'in' '//' f").
(at level 10, x binder, y binder, f at level 200, format "'dlet' x .. y := v 'in' '//' f").
Reserved Notation "'pflet' x , pf := y 'in' f"
(at level 200, f at level 200, format "'pflet' x , pf := y 'in' '//' f").
Reserved Notation "'λ' x .. y , t" (at level 200, x binder, y binder, right associativity, format "'λ' x .. y , '//' t").
Reserved Notation "'λn' x .. y , t" (at level 200, right associativity).
(at level 10, f at level 200, format "'pflet' x , pf := y 'in' '//' f").
Reserved Notation "'λ' x .. y , t" (at level 10, x binder, y binder, t at level 200, format "'λ' x .. y , '//' t").
Reserved Notation "'λn' x .. y , t" (at level 10, t at level 200).
Reserved Notation "x ::> ( max_bitwidth = v )"
(at level 70, no associativity, format "x ::> ( max_bitwidth = v )").
Reserved Notation "r[ l ~> u ]" (l at level 69, format "r[ l ~> u ]").
Expand Down Expand Up @@ -170,7 +170,7 @@ 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").
Reserved Notation "\ x .. y , t" (at level 10, x binder, y binder, t at level 200, 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").

0 comments on commit 991c3c9

Please sign in to comment.