diff options
| author | Théo Zimmermann | 2019-01-23 14:29:49 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-01-23 14:29:49 +0100 |
| commit | 299e445c03c49f3260fca97e135d1fcfb4170751 (patch) | |
| tree | 397c2b5f00016e26b8e6706fb2c56936d2fe548a /kernel/type_errors.mli | |
| parent | 2809b40d2b4c761df0c3ea2cd5bb35357eb99c97 (diff) | |
| parent | 3dcf2f79d422f671aadf441c5318994c9cfea6be (diff) | |
Merge PR #9374: Documentation: ring and field simplify can take no arguments
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions