diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 307e1026b6..6c82aaad0d 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -981,7 +981,7 @@ let vernac_undo n = (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *) let vernac_focus = function - | None -> make_focus 1; print_subgoals () + | None -> traverse_nth_goal 1; print_subgoals () | Some n -> traverse_nth_goal n; print_subgoals () (* Reset the focus to the top of the tree *) |