Respect the default goal selector in toplevel invocations.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index d2b69aaf7d..73086c406e 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -700,7 +700,8 @@ let print_ltac ref =
 let solve default tac =
   let status = Proof_global.with_current_proof begin fun etac p ->
     let with_end_tac = if default then Some etac else None in
-    let (p, status) = Pfedit.solve SelectAll None tac ?with_end_tac p in
+    let g = Proof_bullet.get_default_goal_selector () in
+    let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus Vernacentries.command_focus p in