diff options
| author | Maxime Dénès | 2019-05-27 16:10:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-27 16:10:18 +0200 |
| commit | e005f390312b8900df36aa27bc087e18701c8fcd (patch) | |
| tree | 41d0ceab9484a261c686e665967223c66befca78 /doc/plugin_tutorial/tuto1/src/simple_check.ml | |
| parent | c371b6f0bc6aa75fb3fe138d2bd52bdd189550b1 (diff) | |
| parent | 1e83ae578feea41d34c3ba26a1f74c3c715620a2 (diff) | |
Merge PR #10249: More precise type for export and inlining of private constants
Reviewed-by: gares
Ack-by: maximedenes
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.ml')
0 files changed, 0 insertions, 0 deletions