diff options
author | 2011-12-10 12:53:22 +0000 | |
---|---|---|
committer | 2011-12-10 12:53:22 +0000 | |
commit | dc8f9bb9033702dc7552450c5a3891fd060ee001 (patch) | |
tree | 8d4c4b52cd30f66b2e5e00487116349615fb2bf3 /plugins/extraction/mlutil.ml | |
parent | 61c090d3e5779996c32a9314abe08592df434c30 (diff) |
Extraction: only do the test on generalizable lets for ocaml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14785 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/mlutil.ml')
-rw-r--r-- | plugins/extraction/mlutil.ml | 8 |
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. *) |