Merge PR #6210: More complete not-fully-applied error messages, #6145

2 files changed, 62 insertions, 17 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 1a8ec6d6f6..14b79d73ed 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1380,13 +1380,38 @@ and tactic_of_value ist vle =
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic ist t) in
       Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
-  | VFun (_, _, _,vars,_) ->
-    let numargs = List.length vars in
-    Tacticals.New.tclZEROMSG
-      (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++
-       Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++
-       Pp.str (String.plural numargs "variable") ++ Pp.str " " ++
-       pr_enum Name.print vars ++ Pp.str ".")
+  | VFun (appl,_,vmap,vars,_) ->
+     let tactic_nm =
+       match appl with
+         UnnamedAppl -> "An unnamed user-defined tactic"
+       | GlbAppl apps ->
+          let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in
+          match nms with
+            []    -> assert false
+          | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *)
+     in
+     let numargs = List.length vars in
+     let givenargs =
+       List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in
+     let numgiven = List.length givenargs in
+     Tacticals.New.tclZEROMSG
+       (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++
+          (match numargs with
+            0 -> assert false
+          | 1 ->
+             Pp.str "There is a missing argument for variable " ++
+               (Name.print (List.hd vars))
+          | _ -> Pp.str "There are missing arguments for variables " ++
+             pr_enum Name.print vars) ++ Pp.pr_comma () ++
+          match numgiven with
+            0 ->
+              Pp.str "no arguments at all were provided."
+          | 1 ->
+             Pp.str "an argument was provided for variable " ++
+               Pp.str (List.hd givenargs) ++ Pp.str "."
+          | _ ->
+             Pp.str "arguments were provided for variables " ++
+               pr_enum Pp.str givenargs ++ Pp.str ".")
   | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
index 172612405f..7326f137c2 100644
--- a/test-suite/output/ltac_missing_args.out
+++ b/test-suite/output/ltac_missing_args.out
@@ -1,20 +1,40 @@
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.foo" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.bar" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing arguments for variables y and _.
+The user-defined tactic "Top.bar" was not fully applied:
+There are missing arguments for variables y and _,
+an argument was provided for variable x.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.baz" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.qux" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+The user-defined tactic "Top.mydo" was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable _.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable _,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+The user-defined tactic "Top.rec" was not fully applied:
+There is a missing argument for variable x,
+no arguments at all were provided.
 The command has indeed failed with message:
-A fully applied tactic is expected: missing argument for variable x.
+An unnamed user-defined tactic was not fully applied:
+There is a missing argument for variable x,
+an argument was provided for variable tac.