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/Rewriter.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Rewriter.v') diff --git a/src/Rewriter.v b/src/Rewriter.v index c619d5770..6200e4582 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1255,7 +1255,7 @@ Module Compilers. end%under_lets. Definition assemble_identifier_rewriters {t} (idc : ident t) : value_with_lets t - := eta_ident_cps _ _ idc (fun t' idc' => assemble_identifier_rewriters' t' (rIdent true idc' #idc') (fun _ => id)). + := eta_ident_cps _ _ idc (fun t' idc' => assemble_identifier_rewriters' t' (rIdent true idc' (#idc')) (fun _ => id)). End with_do_again. End with_var. Global Arguments rew_should_do_again {_ _ _ _ _ _} _. -- cgit v1.2.3