diff options
| author | Maxime Dénès | 2017-08-16 09:37:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:37:21 +0200 |
| commit | f052c7fea6b0b9c0628ad77908ede7aac8712bd5 (patch) | |
| tree | 98eed89cf4d4b78806e774716da53ebc1dbbb237 /API/API.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 'API/API.mli')
0 files changed, 0 insertions, 0 deletions