diff options
Diffstat (limited to 'contrib/extraction/miniml.mli')
| -rw-r--r-- | contrib/extraction/miniml.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index e49f4fa68a..67669f8e46 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -43,6 +43,7 @@ type ml_ast = | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy + | MLdummy' | MLcast of ml_ast * ml_type | MLmagic of ml_ast |