diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-21 10:18:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-23 15:32:07 +0200 |
| commit | a3150ecab4c4032ea2c8de96e540ccbae277e233 (patch) | |
| tree | 87cefd41aedde5b73d0350013e4960aaecd2525f /pretyping | |
| parent | 7e4535d62c4f8abc6537206e7abc34f1bb0be69d (diff) | |
Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index c40a24e3b..e1576b971 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) -> |