aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2entries.ml3
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