From c41f5d406f627e94363b4549ef268ffa33e7b681 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Aug 2017 15:01:02 +0200
Subject: Respect the default goal selector in toplevel invocations.

---
 src/tac2entries.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src')

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
-- 
cgit v1.2.3