From 830bca02d66828a4e7633a0c71fbd4fed4b6dff8 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 25 Mar 2004 14:38:50 +0000
Subject: 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
---
 contrib/extraction/haskell.ml | 13 +++++++------
 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 
-- 
cgit v1.2.3