diff options
| author | Maxime Dénès | 2017-09-25 09:51:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-25 09:51:31 +0200 |
| commit | da540472182aa815cbec61b40b23699c191e78bf (patch) | |
| tree | 016211c5f7350d60b529d296b0cad14c5a9a2362 /pretyping | |
| parent | af900539d3d6c28b6f8f0373934d3a1286e9e44f (diff) | |
| parent | a3150ecab4c4032ea2c8de96e540ccbae277e233 (diff) | |
Merge PR #1068: 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 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) -> |