diff options
| author | Pierre-Marie Pédrot | 2015-09-08 11:27:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-08 12:02:50 +0200 |
| commit | 9510a3994210f545119ea35cdad43facededb6a2 (patch) | |
| tree | 08dd8bb0dd3f16894ec96b5df332d1bf7bd35a60 /CHANGES | |
| parent | 99e3bdda7572725f929b77f7349d0a1e06294e94 (diff) | |
Documenting the new behaviour of the Shrink Obligations flag.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -26,6 +26,11 @@ Tactics - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract tactical w.r.t. variables appearing in the body of the proof. +Program + +- The "Shrink Obligations" flag now applies to all obligations, not only those +solved by the automatic tactic. + API - Some functions from pretyping/typing.ml and their derivatives were potential |