diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-27 16:32:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-27 16:59:29 +0100 |
| commit | 5f8c0bfbb04de58a527d373c3994592e5853d4e2 (patch) | |
| tree | 528cfd4057f0aecd08c6357c1cee39a364c9ded4 /kernel/safe_typing.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/safe_typing.ml')
0 files changed, 0 insertions, 0 deletions