diff options
| author | Enrico Tassi | 2019-11-26 11:23:53 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-11-26 11:23:53 +0100 |
| commit | d7879b8566e48aabfdbee5c27bd4c29691352233 (patch) | |
| tree | 286074ecf4016b8fcb89c0fd750557b95f25b64c /kernel/indTyping.mli | |
| parent | 669075119cc0ea8e495a83668fad4f6c1e4f5968 (diff) | |
| parent | f39f25519c89fb88388f8677e7e7f4664aaae7c9 (diff) | |
Merge PR #11173: [ssr] fix «W -- weakening» doc
Reviewed-by: gares
Diffstat (limited to 'kernel/indTyping.mli')
0 files changed, 0 insertions, 0 deletions