diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-05-31 19:13:01 +0200 |
|---|---|---|
| committer | Jade Philipoom <jadep@google.com> | 2018-05-31 19:13:01 +0200 |
| commit | e469076c37fc8b1b6d66eb700e379b9b2a093cb7 (patch) | |
| tree | d65b4249768962239336856b0dd11c216fd2161f /src/Util/Notations.v | |
| parent | c17c32051bc4d481e69b6f9e9b0275a9ccc46db7 (diff) | |
fix over-indented line
Diffstat (limited to 'src/Util/Notations.v')
0 files changed, 0 insertions, 0 deletions