diff options
| author | Son Ho | 2021-11-25 15:23:54 +0100 |
|---|---|---|
| committer | Son Ho | 2021-11-25 15:23:54 +0100 |
| commit | d69093dc3b15a079729b282bbea6b460ffba3a75 (patch) | |
| tree | a43807a1dd802e7ca1fae3fe546826eec68deba3 /.gitignore | |
| parent | 33814c82e8465a0d5f7c6d8f1d39bae087ffb547 (diff) | |
Replace `open Types` by `module T = Types` in Interpreter.ml
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions