diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 6 |
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 -> |