diff options
Diffstat (limited to 'tactics/decl_proof_instr.ml')
| -rw-r--r-- | tactics/decl_proof_instr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index ef2f77069d..e909a1f4fc 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -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 *) |