diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-15 12:16:18 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 13:19:52 +0200 |
commit | 2d4701b4d1bdb0fb4f64dec9ffbd9ad90506ba26 (patch) | |
tree | 54cf74c1318969da0dcaadf4204aefd840ac4dd2 /library/global.ml | |
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 'library/global.ml')
0 files changed, 0 insertions, 0 deletions