diff options
| author | letouzey | 2004-03-25 14:38:50 +0000 |
|---|---|---|
| committer | letouzey | 2004-03-25 14:38:50 +0000 |
| commit | 830bca02d66828a4e7633a0c71fbd4fed4b6dff8 (patch) | |
| tree | 2055ae5eac128ff563115b6145f6625f25e9cca0 | |
| 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
| -rw-r--r-- | contrib/extraction/haskell.ml | 13 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 13 |
2 files changed, 14 insertions, 12 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index abe59c88e9..c55e89a516 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,[]) -> diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 4960f5a698..26f20e43e7 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -211,17 +211,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 2 (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ - spc () ++ str "in") ++ - spc () ++ hov 0 pp_a2)) + (apply + (pp_par par' + (hv 0 + (hov 2 + (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ + spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2))) | MLglob r -> (try let args = list_skipn (projection_arity r) args in |