diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:12:45 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-16 14:12:45 +0000 |
| commit | bf289727d98418069ee3011917393a725d011349 (patch) | |
| tree | 5a636cf9709165fb72ab88f72bb116b60b2f14ec /plugins/extraction/mlutil.ml | |
| parent | 2d0513787170553e2d887c5571b2de02e790a219 (diff) | |
Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-expansions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12936 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2e9fb8bf2..2aee7b8a9 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -320,7 +320,7 @@ let type_expunge env t = | _ -> assert false else t in f t s - else if List.mem (Kill Kother) s then + else if lang () <> Haskell && List.mem (Kill Kother) s then Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t))) else snd (type_decomp (type_weak_expand env t)) @@ -913,13 +913,13 @@ let case_expunge s e = (*s [term_expunge] takes a function [fun idn ... id1 -> c] and a signature [s] and remove dummy lams. The difference with [case_expunge] is that we here leave one dummy lambda - if all lambdas are logical dummy. *) + if all lambdas are logical dummy and the target language is strict. *) let term_expunge s (ids,c) = if s = [] then c else let ids,c = kill_some_lams (List.rev s) (ids,c) in - if ids = [] && List.mem (Kill Kother) s then + if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then MLlam (dummy_name, ast_lift 1 c) else named_lams ids c |