diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-03 14:32:48 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-03 14:40:56 -0400 |
commit | 99376c66e4ff240915455d75cf5901f2d38d8ef6 (patch) | |
tree | ce9335040958cb20568adc839dda787608ba9515 /src/Compilers/Z/BinaryNotationConstants.v | |
parent | ff12e825620f6f6d7bddc24c2d4537936e9236e8 (diff) |
Fix error in generated C notations
It's the final argument, not the second-to-final argument, that needs to
be a particular size
Diffstat (limited to 'src/Compilers/Z/BinaryNotationConstants.v')
0 files changed, 0 insertions, 0 deletions