aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-02-12 10:05:51 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-02-12 10:05:51 +0000
commit1dde0e2599d43b30fd9d5ba4dfb3e358ca232078 (patch)
tree13709e0af1d1b86da49ca56aee0a32eb3aba16cc /contrib/extraction
parent9e89f4d44bf82f2879573057c319c0376c76a698 (diff)
pretty print
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/haskell.ml4
-rw-r--r--contrib/extraction/ocaml.ml4
2 files changed, 4 insertions, 4 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 0dcf58916..04f201edd 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -124,8 +124,8 @@ let rec pp_expr par env args =
(hov 0 (open_par par' ++
hov 2 (str "let" ++ spc () ++ pr_id (List.hd i) ++
str " = " ++ pp_expr false env [] a1 ++ spc () ++
- str "in")
- ++ spc () ++ pp_expr par2 env' [] a2 ++ close_par par'))
+ str "in") ++
+ spc () ++ hov 0 (pp_expr par2 env' [] a2) ++ close_par par'))
| MLglob r ->
apply (pp_global r)
| MLcons (r,[]) ->
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index c19131757..60b0b9689 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -191,8 +191,8 @@ let rec pp_expr par env args =
apply
(hov 0 (open_par par' ++
hov 2 (str "let " ++ pr_id (List.hd i) ++ str " =" ++ spc ()
- ++ pp_expr false env [] a1 ++ spc () ++ str "in")
- ++ spc () ++ pp_expr par2 env' [] a2 ++ close_par par'))
+ ++ pp_expr false env [] a1 ++ spc () ++ str "in") ++
+ spc () ++ hov 0 (pp_expr par2 env' [] a2) ++ close_par par'))
| MLglob r ->
apply (pp_global r)
| MLcons (r,[]) ->