diff options
Diffstat (limited to 'library')
| -rw-r--r--[-rwxr-xr-x] | library/nametab.ml | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index e4a8ee9956..e4a8ee9956 100755..100644 --- a/library/nametab.ml +++ b/library/nametab.ml |