diff options
| author | Hugo Herbelin | 2017-09-21 10:18:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-23 15:32:07 +0200 |
| commit | a3150ecab4c4032ea2c8de96e540ccbae277e233 (patch) | |
| tree | 87cefd41aedde5b73d0350013e4960aaecd2525f /kernel | |
| parent | 7e4535d62c4f8abc6537206e7abc34f1bb0be69d (diff) | |
Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions