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.ml | |
parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) |
Mention requiring extraction/funind in CHANGES
Diffstat (limited to 'library/nametab.ml')
0 files changed, 0 insertions, 0 deletions