diff options
| author | Pierre-Marie Pédrot | 2016-06-15 12:16:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-16 13:19:52 +0200 |
| commit | 2d4701b4d1bdb0fb4f64dec9ffbd9ad90506ba26 (patch) | |
| tree | 54cf74c1318969da0dcaadf4204aefd840ac4dd2 /kernel | |
| parent | dcf4d3e28813e09fc71f974b79ddf42d2e525976 (diff) | |
Fixing the checker.
This is a stupid fix that only allows to take into account the change in
memory layout. The check will simply fail when encountering a unguarded
inductive or (co)fixpoint.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions