diff options
| author | Maxime Dénès | 2019-05-27 13:25:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-27 13:25:48 +0200 |
| commit | c371b6f0bc6aa75fb3fe138d2bd52bdd189550b1 (patch) | |
| tree | 747f6c77ecdbd474164cba7b6d7b7b568c743674 /kernel/indTyping.ml | |
| parent | 13034bc2a322d250a971c9cc73881a34f9d64025 (diff) | |
| parent | e3df4fce6ec981140bbba5f6ac46292dad215754 (diff) | |
Merge PR #10241: Update README.md / add SUPPORT.md file.
Reviewed-by: maximedenes
Diffstat (limited to 'kernel/indTyping.ml')
0 files changed, 0 insertions, 0 deletions