diff options
| author | Théo Zimmermann | 2018-08-02 12:18:40 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-02 12:18:40 +0200 |
| commit | 75a9f58381ec3ac0f0f108dd71bcf69774da9023 (patch) | |
| tree | d2b3c6795e4be0f94d0b15dcd459d1ac01b4ab57 /kernel/type_errors.ml | |
| parent | bc06df20f659867ebb39d3205974062754fe8460 (diff) | |
| parent | fcf7bd199413b40b899c951952e1d79757f1f08d (diff) | |
Merge PR #8176: Improved grammar and spelling in chapters 'Type Classes', 'Omega' and 'Micromega' of the Reference Manual.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions