diff options
| author |  Tej Chajed <tchajed@mit.edu> | 2017-09-06 09:13:42 -0400 |
|---|---|---|
| committer |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-10-02 17:30:00 +0200 |
| commit | 8bf34547d21d417140b726fab5fdbf8625c5be95 (patch) | |
| tree | d49fdf9db0b284b4bf4f01b9d816d6e39dd4679f /library/nametab.mli | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) | |
Mention requiring extraction/funind in CHANGES
Diffstat (limited to 'library/nametab.mli')
0 files changed, 0 insertions, 0 deletions