diff options
| author | aspiwack | 2013-11-04 18:08:46 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-04 18:08:46 +0000 |
| commit | 5f4a61935e048a8e4490f5610e551d8844a373c4 (patch) | |
| tree | 7a53bac5bdb769224b4b7057940573770e450eb3 /kernel/type_errors.ml | |
| parent | e3d3d73dfca0576cb25ce555cc445c657baecb19 (diff) | |
Fix ltac's progress tactical: requires progress in each goal.
Proofview.tclPROGRESS considers that a tactic that changes the list of goal progresses, under this semantics, "progress auto" succeeds if its applied to two goals and solves the first one but not the second one. This would break backwards compatibility.
Spotted in Fermat4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17058 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions