Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4300 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 5a47410b29..a343b37a60 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -174,9 +174,9 @@ let pr_let_binder pr x a =
   hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ brk(0,1) ++ pr ltop a)
 
 let rec extract_prod_binders = function
-  | CLetIn (loc,na,b,c) ->
+  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_prod_binders c in
-      LocalRawDef (na,b) :: bl, c
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c
   | CProdN (loc,[],c) ->
       extract_prod_binders c
   | CProdN (loc,(nal,t)::bl,c) ->
@@ -185,9 +185,9 @@ let rec extract_prod_binders = function
   | c -> [], c
 
 let rec extract_lam_binders = function
-  | CLetIn (loc,na,b,c) ->
+  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_lam_binders c in
-      LocalRawDef (na,b) :: bl, c
+      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c
   | CLambdaN (loc,[],c) ->
       extract_lam_binders c
   | CLambdaN (loc,(nal,t)::bl,c) ->