diff options
author | 2017-02-04 14:47:53 +0100 | |
---|---|---|
committer | 2017-03-24 12:22:21 +0100 | |
commit | 6899bace8e617f38fadce0b4b660d951d73af5d0 (patch) | |
tree | ed55d3abcb239da96efcb1744acb0fa457d2d777 /kernel/modops.mli | |
parent | b496309c7d4707a4377c72b0543faa025d993589 (diff) |
Applying same convention as in Definition for parsing type in a let in.
Diffstat (limited to 'kernel/modops.mli')
0 files changed, 0 insertions, 0 deletions