diff options
| author | Hugo Herbelin | 2017-07-14 23:19:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-07-15 11:40:25 +0200 |
| commit | 7b88d786d16c54fe8ad2d0802a1551bfc9265b9e (patch) | |
| tree | eac687184adf40091652e0b747cea34e706c914d /API/API.mli | |
| parent | e3eb17a728d7b6874e67462e8a83fac436441872 (diff) | |
Fixing #5648 (too early decision of tagging ident as keyword in html coqdoc).
Fix proposed by the reporter, Vincent Laporte.
Note that for LaTeX output, the selection of a keyword was already
done after checking if the ident is recognized as a Coq ident by
coqtop.
Incidentally, being now explicit on an wildcard-catching of exceptions.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions