diff options
| author | Matthieu Sozeau | 2016-11-04 15:55:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-08 14:56:22 +0100 |
| commit | b385fbbbb7868f0994d5ec00cb918cea1e8f18cf (patch) | |
| tree | 7f7e4585f2a9a93366f7c316f40c36818f4c7b2b /kernel/inductive.mli | |
| parent | 6f30019bfd99a0125fdc12baf8b6c04169701fb7 (diff) | |
Use pf_get_type_of to avoid blowup in pose proof of large proof terms
Diffstat (limited to 'kernel/inductive.mli')
0 files changed, 0 insertions, 0 deletions