diff options
| author | Maxime Dénès | 2018-12-04 15:07:33 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-04 15:07:33 +0100 |
| commit | 87c98872a68919ed9171ee4e0982519145b3e30b (patch) | |
| tree | 5a4b7ebdc5776674ec7a066ede1ac5bb7d740422 /pretyping/typeclasses_errors.mli | |
| parent | fe81b1a6f813fe21f0cc21ede761acae64c7b026 (diff) | |
| parent | 5b65f456a8bd7378bbcf931c0ed4817da112992a (diff) | |
Merge PR #9053: Document code owner team creation.
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions