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).

---
 test-suite/bugs/closed/5749.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/5749.v

(limited to 'test-suite')

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)).
-- 
cgit v1.2.3