diff options
| -rw-r--r-- | translate/ppconstrnew.ml | 8 |
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) -> |