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/Language.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Language.v') diff --git a/src/Language.v b/src/Language.v index eb64e0f2e..b4fc4ed2d 100644 --- a/src/Language.v +++ b/src/Language.v @@ -782,7 +782,7 @@ Module Compilers. Notation "\ x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope. Notation "'λ' x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope. Notation "'expr_let' x := A 'in' b" := (LetIn A (fun x => b%expr)) : expr_scope. - Notation "'$' x" := (Var x) (at level 10, format "'$' x") : expr_scope. + Notation "'$' x" := (Var x) : expr_scope. Notation "### x" := (Ident x) : expr_scope. End Notations. End expr. -- cgit v1.2.3