diff options
Diffstat (limited to 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 451272d554..a5a6564873 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -128,6 +128,7 @@ and ml_ast = | MLmagic of ml_ast | MLuint of Uint63.t | MLfloat of Float64.t + | MLparray of ml_ast array * ml_ast and ml_pattern = | Pcons of GlobRef.t * ml_pattern list |