aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
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 /src/Util/Equality.v
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.
Diffstat (limited to 'src/Util/Equality.v')
0 files changed, 0 insertions, 0 deletions