From 0fd335e25cdf37d734f279bc0bd562809bddb86f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 3 Sep 2003 17:39:10 +0000
Subject: 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
---
 translate/ppconstrnew.ml | 8 ++++----
 1 file 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) ->
-- 
cgit v1.2.3