diff options
| author | Johannes Kloos | 2017-10-24 01:06:05 +0200 |
|---|---|---|
| committer | Johannes Kloos | 2017-10-24 01:06:05 +0200 |
| commit | e26b67436d12da63a11f0727c5b5895dfd03d249 (patch) | |
| tree | b6915791975b3bf1e3c4256a2f84f11a366ef37b /kernel/type_errors.ml | |
| parent | 16061426080400749ca96fb140dd42042e51b7b9 (diff) | |
Documentation: Add various basic constructs to the index.
This was mentioned in #5631 as well. Now, forall, fun
and casts have index entries.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions