diff options
| -rw-r--r-- | plugins/extraction/extraction.ml | 6 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.ml | 8 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.mli | 2 |
3 files changed, 9 insertions, 7 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 532ed69e8..219b3913f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -586,9 +586,9 @@ let rec extract_term env mle mlt c args = let c1' = extract_term env mle a c1 [] in (* The type of [c1'] is generalized and stored in [mle]. *) let mle' = - if not_generalizable c1' - then Mlenv.push_type mle a - else Mlenv.push_gen mle a + if generalizable c1' + then Mlenv.push_gen mle a + else Mlenv.push_type mle a in MLletin (Id id, c1', extract_term env' mle' mlt c2 args') with NotDefault d -> 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. *) diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 21a3d6e19..029e8cf46 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -27,7 +27,7 @@ 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 +val generalizable : ml_ast -> bool (*s ML type environment. *) |