diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:38 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:38 +0200 |
| commit | 3a420f4ad929e8372d32c735fd0fd89dfc0346a1 (patch) | |
| tree | 943a01d103c1296dc7c07cb188af994354c4d9a3 /tactics/decl_proof_instr.ml | |
| parent | 1769cbaddea77112dd6f336316d8eb9a0945a1e6 (diff) | |
| parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) | |
Merge commit 'upstream/8.2.pl1+dfsg'
Diffstat (limited to 'tactics/decl_proof_instr.ml')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 2d0395a3..62a8ddfc 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *) open Util open Pp @@ -174,7 +174,7 @@ let mark_proof_tree_as_done pt = let mark_as_done pts = map_pftreestate (fun _ -> mark_proof_tree_as_done) - (traverse 0 pts) + (up_to_matching_rule is_focussing_command pts) (* post-instruction focus management *) |