From 00658ba40fee7911486d6d6ccac36ab430b0096a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Nov 2023 05:27:21 +0100 Subject: [PATCH] Moving at level 10 notations which were originally at level 200. (#1695) This follows what was done for notations at level binder_constr in Coq PR #18014. --- src/Util/Notations.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 7abe015f23..8bbe6ce902 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -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 ]"). @@ -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").