diff options
| author | Maxime Dénès | 2017-11-13 11:21:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 11:21:41 +0100 |
| commit | a7df689e73dd396dafdbb4891d534b7fa5cb0fc8 (patch) | |
| tree | 8682480b7dc5cc4557344490968166061e656b93 /interp/interp.mllib | |
| parent | 1f9dcdee40d95ee56ef91876579f2c059939e04a (diff) | |
| parent | fb08d2d78c80f384e8ac2b7a9563b6c6720608f4 (diff) | |
Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.
Diffstat (limited to 'interp/interp.mllib')
| -rw-r--r-- | interp/interp.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/interp.mllib b/interp/interp.mllib index 6d290a325c..e3500cfeac 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,4 @@ +Tactypes Stdarg Genintern Constrexpr_ops |