diff options
| author | Pierre-Marie Pédrot | 2018-09-24 14:34:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-24 14:34:16 +0200 |
| commit | 1946a98e9f6e8cf9a619f01c406d9fc37dd56641 (patch) | |
| tree | 193f53eb55c8f88e91eb995ff3f52fce65c2bb38 /kernel/nativecode.ml | |
| parent | c6d3e0ba94ea093d1f51b374e52f49e08aa25d9a (diff) | |
| parent | 27c7b5f2eaada92897c51d974c86d148213bd475 (diff) | |
Merge PR #8499: [api] Deprecate constructors of deprecated datatypes.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions