diff options
| author | Pierre-Marie Pédrot | 2015-08-22 20:36:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-08 12:02:50 +0200 |
| commit | 99e3bdda7572725f929b77f7349d0a1e06294e94 (patch) | |
| tree | e078a48d2363c38f411f32aa3bdccd747071d52f /kernel/nativecode.mli | |
| parent | dcd0e227295d1250234e027ba11289247de64e37 (diff) | |
All Program obligations now respect the Shrink Obligation flag.
This allows to reduce the dependencies of subproofs generated by any sequence
of tactics. Grants wish #4327.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions