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 | |
| parent | af900539d3d6c28b6f8f0373934d3a1286e9e44f (diff) | |
| parent | a3150ecab4c4032ea2c8de96e540ccbae277e233 (diff) | |
Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).
| -rw-r--r-- | pretyping/glob_ops.ml | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5749.v | 18 |
2 files changed, 20 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) -> diff --git a/test-suite/bugs/closed/5749.v b/test-suite/bugs/closed/5749.v new file mode 100644 index 0000000000..81bfe351c5 --- /dev/null +++ b/test-suite/bugs/closed/5749.v @@ -0,0 +1,18 @@ +(* Checking computation of free vars of a term for generalization *) + +Definition Decision := fun P : Prop => {P} + {~ P}. +Class SetUnfold (P Q : Prop) : Prop := Build_SetUnfold { set_unfold : P <-> Q +}. + +Section Filter_Help. + + Context {A: Type}. + Context (fold_right : forall A B : Type, (B -> A -> A) -> A -> list B -> A). + Definition lType2 := (sigT (fun (P : A -> Prop) => forall a, Decision (P +a))). + Definition test (X: lType2) := let (x, _) := X in x. + + Global Instance foo `{fhl1 : list lType2} m Q: + SetUnfold (Q) + (fold_right _ _ (fun (s : lType2) => let (P, _) := s in and (P +m)) (Q) (fhl1)). |