4 files changed, 19 insertions, 18 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 2ea0f60ebc..86c983bdd9 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 8a0764975d..d8bd166208 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 1f6ebaf448..c79d5b389f 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 :
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 18348bc113..20f117ff4f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1394,7 +1394,13 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
       else
         Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
-    | _ -> fail
+    | (VFun(appl,trace,olfun,[],body)) ->
+      let extra_args = List.length largs in
+      Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++
+                                str (string_of_int extra_args) ++
+                                str " extra " ++ str (String.plural extra_args "argument") ++
+                                str ".")
+    | VRec(_,_) -> fail
   else fail
 
 (* Gives the tactic corresponding to the tactic value *)