aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Notations.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-14 11:48:12 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-05-14 11:48:12 -0400
commitff0e6450bf741d18e595d67d3a97ca3cf34cfe82 (patch)
treefe52dd4cf92460ed04ba3a060d30e4fb84b92531 /src/Util/Notations.v
parent189a0eba8a2c8ddfbb27d92f2f461f21864815e3 (diff)
Ooops, I mixed up Bind Scope and Delimit Scope
Diffstat (limited to 'src/Util/Notations.v')
0 files changed, 0 insertions, 0 deletions