diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 18:08:46 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 18:08:46 +0000 |
| commit | 5f4a61935e048a8e4490f5610e551d8844a373c4 (patch) | |
| tree | 7a53bac5bdb769224b4b7057940573770e450eb3 /doc/refman | |
| 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 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index ae5653c14..13b2d387b 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -371,7 +371,8 @@ We can check if a tactic made progress with: {\tt progress} {\tacexpr} \end{quote} {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is -applied. If the application of $v$ produced subgoals equal to the +applied to each focued subgoal independently. If the application of +$v$ to one of the focused subgoal produced subgoals equal to the initial goals (up to syntactical equality), then an error of level 0 is raised. |