diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-14 11:48:12 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-05-14 11:48:12 -0400 |
commit | ff0e6450bf741d18e595d67d3a97ca3cf34cfe82 (patch) | |
tree | fe52dd4cf92460ed04ba3a060d30e4fb84b92531 /src/Util/Notations.v | |
parent | 189a0eba8a2c8ddfbb27d92f2f461f21864815e3 (diff) |
Ooops, I mixed up Bind Scope and Delimit Scope
Diffstat (limited to 'src/Util/Notations.v')
0 files changed, 0 insertions, 0 deletions