aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBenjamin Barenblat <bbaren@google.com>2019-04-26 17:10:05 -0400
committerBenjamin Barenblat <bbaren@google.com>2019-04-26 17:10:05 -0400
commit6de992d169e076f2e579e14b0d64ff68616e04b0 (patch)
tree8e9d90a802227b60ed1f4b387ddec8d4084e530d
parent4483d41d6a510e01041f05546643934c9d2a887b (diff)
Clean up notations after bbv removalHEADmaster
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.
-rw-r--r--src/Language.v2
-rw-r--r--src/Rewriter.v2
-rw-r--r--src/Util/Notations.v7
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").