diff options
| author | Théo Zimmermann | 2018-08-02 12:20:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-02 12:20:33 +0200 |
| commit | f18c948a913f1b07417adf5f21c987513d4f8635 (patch) | |
| tree | c3ffbd7f7fc8455bea8f6968c96d2a29512ea59b /kernel/type_errors.mli | |
| parent | 75a9f58381ec3ac0f0f108dd71bcf69774da9023 (diff) | |
| parent | ab02e2689b44d34d50c8303d8bc63bec7be8a433 (diff) | |
Merge PR #8144: Improved grammar and spelling for chapters 'Utilities' and 'CoqIDE' of the Reference Manual.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions