diff options
| author | Gaëtan Gilbert | 2019-10-18 20:30:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-18 20:30:43 +0200 |
| commit | c5f2b14020ea1fb2b11321f1daa00abe8dec3477 (patch) | |
| tree | f17e83a8d3555c8b74eeb15c39d853c06240db51 /test-suite | |
| parent | fe4e6aae2f4ae86a2f1f7262709ace8d31869c8c (diff) | |
| parent | 5c5790d587ad425a882ea8bcdcf28d5ac046aaa3 (diff) | |
Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in the kernel.
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_10904.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_10904.v b/test-suite/bugs/closed/bug_10904.v new file mode 100644 index 0000000000..32b25ff726 --- /dev/null +++ b/test-suite/bugs/closed/bug_10904.v @@ -0,0 +1,8 @@ +Definition a := fun (P:SProp) (p:P) => p. + +Lemma foo : (let k := a in let k' := a in fun (x:nat) y => x) = (let k := a in fun x y => y). +Proof. + Fail reflexivity. + match goal with |- ?l = _ => exact_no_check (eq_refl l) end. +Fail Qed. +Abort. |