diff options
| author | Pierre-Marie Pédrot | 2020-02-11 10:29:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-11 10:29:44 +0100 |
| commit | ec3d9ae1210e57271142ae91585b520c2978a4e9 (patch) | |
| tree | 587d77c1b430446749163ff309dc80f243c1e204 /kernel/type_errors.mli | |
| parent | 056c66fef0def03c495b17b54dd3ff5c706337a4 (diff) | |
| parent | 9c548090b0b27ed80cb6463852f103cf74edc06d (diff) | |
Merge PR #11538: Remove many unsafe_type_of uses
Reviewed-by: Matafou
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions