diff options
author | Son Ho | 2021-12-08 11:24:10 +0100 |
---|---|---|
committer | Son Ho | 2021-12-08 11:24:10 +0100 |
commit | b8bd4db2aed58c6e8dc7578156e753edbc9c9cb3 (patch) | |
tree | dd5e321ce06567d3d83340f83fe6e6ffe9df701a /src/Identifiers.ml | |
parent | d7cd9ebc3dfc1fbe0782e28f66e13629594dc1e9 (diff) |
Make the map visitors non-polymorphic
Diffstat (limited to 'src/Identifiers.ml')
0 files changed, 0 insertions, 0 deletions