diff options
| author | Hugo Herbelin | 2015-03-07 14:35:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-03-07 14:35:05 +0100 |
| commit | 9ea96eb933c690679748ab3e55488662e01b71ec (patch) | |
| tree | 5a73a3fdb88d5944f7701eb1bb76fddfee410a79 /kernel | |
| parent | a684010f1a926c6fa1649b1a6c386645bd520a21 (diff) | |
Test for #4035 (dependent destruction from Ltac).
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions