From a3150ecab4c4032ea2c8de96e540ccbae277e233 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Sep 2017 10:18:41 +0200
Subject: Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).

---
 pretyping/glob_ops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index c40a24e3b7..e1576b9713 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -234,7 +234,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     let acc = Option.fold_left (f v') acc rtntypopt in
     List.fold_left fold_pattern acc pl
   | GLetTuple (nal,rtntyp,b,c) ->
-    f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c
+    f (List.fold_right (Name.fold_right g) nal v)
+      (f v (fold_return_type_with_binders f g v acc rtntyp) b) c
   | GIf (c,rtntyp,b1,b2) ->
     f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
   | GRec (_,idl,bll,tyl,bv) ->
-- 
cgit v1.2.3