diff options
Diffstat (limited to 'plugins/extraction/mlutil.mli')
| -rw-r--r-- | plugins/extraction/mlutil.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 452fd46c0..21a3d6e19 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -27,6 +27,8 @@ val needs_magic : ml_type * ml_type -> bool val put_magic_if : bool -> ml_ast -> ml_ast val put_magic : ml_type * ml_type -> ml_ast -> ml_ast +val not_generalizable : ml_ast -> bool + (*s ML type environment. *) module Mlenv : sig |