diff options
author | Son Ho | 2023-11-22 11:14:13 +0100 |
---|---|---|
committer | Son Ho | 2023-11-22 11:14:13 +0100 |
commit | 724ff98309444537cf03ba7ccab06d432e2eb376 (patch) | |
tree | b9b86698fa2ecb66440eda609f9855ebf2fd474e /compiler/Extract.ml | |
parent | 84a505ed9f193885175308ecc837922a41176b5b (diff) |
Use NameMatcher.NameMatcherMap instead of associative lists
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions