diff options
| author |  Johannes Kloos <jkloos@mpi-sws.org> | 2017-10-25 22:57:06 +0200 |
|---|---|---|
| committer | Johannes Kloos <jkloos@mpi-sws.org> | 2017-10-25 22:57:06 +0200 |
| commit | 258c6a766d6f5d623925211694e7cede001f872e (patch) | |
| tree | b973099fb42803f9544a86540d2f9de9747e7740 /kernel/cemitcodes.mli | |
| parent | 5a7ca0b267e8531137d302b9c54b41bed097085f (diff) | |
Rename \Tree to \NatTree
Diffstat (limited to 'kernel/cemitcodes.mli')
0 files changed, 0 insertions, 0 deletions