diff options
| author | Pierre-Marie Pédrot | 2020-02-24 18:11:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-24 18:11:58 +0100 |
| commit | 00a3dcc11342e1304f078e1457dcfd118dc4e573 (patch) | |
| tree | 8bfedced5772616dbe97f80a3ae29cff9180f3b5 /kernel/constr.ml | |
| parent | 5fd281945bdc60c2a88f60503663df32920ef83b (diff) | |
| parent | 5d535c7c624cc4ebae23b173254ba6492b33bee2 (diff) | |
Merge PR #11623: Deprecate unsafe_type_of
Reviewed-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/constr.ml')
0 files changed, 0 insertions, 0 deletions