aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/mlutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/mlutil.ml')
-rw-r--r--plugins/extraction/mlutil.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 78afefa98..c244e046d 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -116,9 +116,11 @@ let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
-let not_generalizable = function
- | MLapp _ -> true
- | _ -> false (* TODO, this is just an approximation *)
+let generalizable a =
+ lang () <> Ocaml ||
+ match a with
+ | MLapp _ -> false
+ | _ -> true (* TODO, this is just an approximation for the moment *)
(*S ML type env. *)