diff options
| author | Emilio Jesus Gallego Arias | 2017-04-08 23:34:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-25 00:31:39 +0200 |
| commit | d062642d6e3671bab8a0e6d70e346325558d2db3 (patch) | |
| tree | 80c3ea911c9df1eb8bf7f0c7edb998e1dde5a7f9 /interp/notation.ml | |
| parent | 6eb42e53ffafd9aed3c12805c6a228acccc03827 (diff) | |
[location] Be consistent with type module qualification
Thanks to @gasche
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions