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

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. *)