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

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 532ed69e88..219b3913fa 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 ->