diff options
| author | Guillaume Melquiond | 2015-07-31 17:28:40 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-07-31 17:28:40 +0200 |
| commit | 71e0a34f89d03787003df1a30bb793bd71ebb775 (patch) | |
| tree | 4357cdaa3b229a8780eb07ff798aa966236686bd /kernel/type_errors.mli | |
| parent | 947206269dc31bb6b919fce935e1748bc440d960 (diff) | |
Fix typos in the Extraction part of the reference manual.
In particular, fix the name of all the user contributions.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions