aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorThéo Zimmermann2018-04-04 09:47:18 +0200
committerThéo Zimmermann2018-04-04 09:47:18 +0200
commitbec815511e2bff57637bd24fb7accd3238b6db3c (patch)
treedfaa58ba93d0f7c447827b687dd72c7467939c02 /kernel/type_errors.mli
parent7e51ffdaf4340a67c254be7800eb8c68c5d78f2c (diff)
parentf84eda17d1e1d15248bab4fb41941b2d6da77ddb (diff)
Merge PR #7047: Sphinx doc chapter 24
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions