diff options
Diffstat (limited to 'test-suite/bugs/closed/5749.v')
-rw-r--r-- | test-suite/bugs/closed/5749.v | 18 |
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 00000000..81bfe351 --- /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)). |