diff options
| author | Maxime Dénès | 2017-11-27 16:55:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-27 16:55:05 +0100 |
| commit | 68061d8d464d0c62442675897c9c5f6db8d2b2e4 (patch) | |
| tree | d0b0b312054b505a5bd5d1c9da71de70f9cc2f93 /kernel/nativelib.ml | |
| parent | 2fcbfcfe8066bcf7ee40830bb9043b0cfd754e63 (diff) | |
| parent | 83c63a5075fb55e4e3291e163417bcffaf009dcd (diff) | |
Merge PR #6207: [stm] Allow delayed constant in interactive mode.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions