aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/haskell.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-28 03:20:04 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-28 03:20:04 +0000
commit59aea502e26b4015a7339a3bc9b92af48932170d (patch)
treef7c83daee366779f87922cfa34d3f9b65d8bb3fe /contrib/extraction/haskell.ml
parent20e13100d0042a97c39ee680ea8a604c034f3fb6 (diff)
bug pp letin + un inductif constant n'est pas un record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3324 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/haskell.ml')
-rw-r--r--contrib/extraction/haskell.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 283309b59..aac1374d1 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -113,8 +113,8 @@ let rec pp_expr par env args =
and pp_a1 = pp_expr false env [] a1
and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
hv 0
- (hv 0
- (pp_par par
+ (pp_par par
+ (hv 0
(hov 2 (str "let" ++ pp_id ++ str " = " ++ pp_a1) ++
spc () ++ str "in") ++
spc () ++ hov 0 pp_a2))