diff options
| author | Son Ho | 2023-06-26 18:40:47 +0200 |
|---|---|---|
| committer | Son Ho | 2023-06-26 18:40:47 +0200 |
| commit | 4cc411a30b19f5c5eea67b2e4da232337af8f12b (patch) | |
| tree | 4a9ada0f798c01eeac5431e8da5daefa74469110 /compiler/Names.ml | |
| parent | 87fd14e74fe00752df7759372093543ae77a51ae (diff) | |
Generalize some definitions
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions