Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).

3 files changed, 12 insertions, 17 deletions

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 2ea0f60eb..86c983bdd 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -388,16 +388,7 @@ let vernac_solve n info tcom b =
     p,status) in
     if not status then Feedback.feedback Feedback.AddedAxiom
 
-let pr_range_selector (i, j) =
-  if Int.equal i j then int i
-  else int i ++ str "-" ++ int j
-
-let pr_ltac_selector = function
-| SelectNth i -> int i ++ str ":"
-| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
-    str "]" ++ str ":"
-| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
-| SelectAll -> str "all" ++ str ":"
+let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
 
 VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
 | [ toplevel_selector(s) ] -> [ s ]
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 8a0764975..d8bd16620 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -477,12 +477,14 @@ type 'a extra_genarg_printer =
     if Int.equal i j then int i
     else int i ++ str "-" ++ int j
 
-  let pr_goal_selector = function
-    | SelectNth i -> int i ++ str ":"
-    | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
-        str "]" ++ str ":"
-    | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
-    | SelectAll -> str "all" ++ str ":"
+let pr_goal_selector toplevel = function
+  | SelectNth i -> int i ++ str ":"
+  | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
+  | SelectId id -> str "[" ++ Id.print id ++ str "]:"
+  | SelectAll -> assert toplevel; str "all:"
+
+let pr_goal_selector ~toplevel s =
+  (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s
 
   let pr_lazy = function
     | General -> keyword "multi"
@@ -988,7 +990,7 @@ type 'a extra_genarg_printer =
               keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
             | TacComplete t ->
               pr_tac (lcomplete,E) t, lcomplete
-            | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom
+            | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
             | TacAtom (loc,t) ->
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 1f6ebaf44..c79d5b389 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -53,6 +53,8 @@ type pp_tactic = {
   pptac_prods : grammar_terminals;
 }
 
+val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t
+
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 val pr_with_occurrences :