Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5749.v b/test-suite/bugs/closed/5749.v
new file mode 100644
index 000000000..81bfe351c
--- /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)).