diff options
| -rw-r--r-- | src/Language.v | 2 | ||||
| -rw-r--r-- | src/Rewriter.v | 2 | ||||
| -rw-r--r-- | src/Util/Notations.v | 7 |
3 files changed, 3 insertions, 8 deletions
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. 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 {_ _ _ _ _ _} _. diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 9549e0ba6..63f529762 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -171,15 +171,10 @@ Reserved Notation "'return' x" (at level 70, format "'return' x"). Reserved Notation "f x" (only printing, at level 10, left associativity). (* TODO: Remove this next one if and when we drop support for Coq 8.7; it's present in the stdlib in 8.8 *) Reserved Notation "{ x & P }" (at level 0, x at level 99). -(* 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" (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"). - -(* TODO: Remove these when https://github.com/mit-plv/bbv/pull/13 is merged *) -Reserved Notation "# x" (at level 0, format "# x"). |