diff options
author | 2015-02-27 16:32:38 +0100 | |
---|---|---|
committer | 2015-02-27 16:59:29 +0100 | |
commit | 5f8c0bfbb04de58a527d373c3994592e5853d4e2 (patch) | |
tree | 528cfd4057f0aecd08c6357c1cee39a364c9ded4 /kernel/reduction.ml | |
parent | 172388eab4f34da71d82c4fab269bd6426c73853 (diff) |
Hack so that refine_no_check accepts an argument which is a match on an
inductive type with let-in in the arity (until logic.ml disappears).
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions