diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-25 14:38:50 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-25 14:38:50 +0000 |
| commit | 830bca02d66828a4e7633a0c71fbd4fed4b6dff8 (patch) | |
| tree | 2055ae5eac128ff563115b6145f6625f25e9cca0 /contrib/extraction/haskell.ml | |
| parent | dcadbeec1234fa8eacf528d088adb0e523077b9c (diff) | |
Selon les optims, le let-in peut avoir maintenant des args
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5566 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/haskell.ml')
| -rw-r--r-- | contrib/extraction/haskell.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index abe59c88e..c55e89a51 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -111,17 +111,18 @@ let rec pp_expr par env args = let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in apply (pp_par par' st) | MLletin (id,a1,a2) -> - assert (args=[]); let i,env' = push_vars [id] env in let pp_id = pr_id (List.hd i) and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in hv 0 - (pp_par par - (hv 0 - (hov 5 (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ - spc () ++ str "in") ++ - spc () ++ hov 0 pp_a2)) + (apply + (pp_par par' + (hv 0 + (hov 5 + (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ + spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2))) | MLglob r -> apply (pp_global r) | MLcons (r,[]) -> |