diff options
| author | Pierre-Marie Pédrot | 2019-06-25 11:54:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-08 20:46:19 +0200 |
| commit | 3ce18524834bb9ff7a9ea14c3f1659decb63af76 (patch) | |
| tree | 2e242754d41b804c1d94a74b2c93b0565bd5d73d /kernel/safe_typing.mli | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
Do not export side-effects of polymorphic definitions.
This is the last call to the kernel that makes a difference between opaque
definitions depending on their polymorphic status.
Diffstat (limited to 'kernel/safe_typing.mli')
0 files changed, 0 insertions, 0 deletions