diff options
| author | Hugo Herbelin | 2019-05-21 14:18:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-21 20:48:42 +0200 |
| commit | c7f1470c69bf5e8e823550fe94c28fc5fa33e712 (patch) | |
| tree | 8cdbde50b7ee3f1e80d6cecaf6d005dfe78877ac /kernel | |
| parent | d14be61b4468573d7aa184fe6c8a0a7c8d5a0044 (diff) | |
Adding test for old bug fixed in 8.5 (wrong implicit arguments in fixpoint).
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions