diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:37:21 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:37:21 +0200 |
commit | f052c7fea6b0b9c0628ad77908ede7aac8712bd5 (patch) | |
tree | 98eed89cf4d4b78806e774716da53ebc1dbbb237 /kernel/safe_typing.mli | |
parent | f0b4757d291ce3e07c8ccfcd4217d204fd2059ba (diff) | |
parent | f3bb625fb2d118168042b97162e1ece1bda4a039 (diff) |
Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wrongly tagged as keywords
Diffstat (limited to 'kernel/safe_typing.mli')
0 files changed, 0 insertions, 0 deletions