From 028db341f3cb924c2d1b3a9e0fa5666425130f90 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 9 Feb 2017 11:15:51 -0500
Subject: Report missing tactic arguments in error message

Augments "A fully applied tactic is expected" with the list of missing
arguments to the tactic. Addresses [bug
5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
---
 plugins/ltac/tacinterp.ml               |  9 ++++++++-
 test-suite/output/ltac_missing_args.out | 21 +++++++++++++++++++++
 test-suite/output/ltac_missing_args.v   | 19 +++++++++++++++++++
 3 files changed, 48 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/output/ltac_missing_args.out
 create mode 100644 test-suite/output/ltac_missing_args.v

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index aa646aa517..54bec39670 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1422,7 +1422,14 @@ 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 _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
+  | 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 pr_name vars ++ 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
     tactic_of_value ist tac
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
new file mode 100644
index 0000000000..ae3fd7acc7
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.out
@@ -0,0 +1,21 @@
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected:
+missing arguments for variables y and _.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable _.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
+The command has indeed failed with message:
+Error: A fully applied tactic is expected: missing argument for variable x.
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
new file mode 100644
index 0000000000..8ecd97aa56
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.v
@@ -0,0 +1,19 @@
+Ltac foo x := idtac x.
+Ltac bar x := fun y _ => idtac x y.
+Ltac baz := foo.
+Ltac qux := bar.
+Ltac mydo tac := tac ().
+Ltac rec x := rec.
+
+Goal True.
+  Fail foo.
+  Fail bar.
+  Fail bar True.
+  Fail baz.
+  Fail qux.
+  Fail mydo ltac:(fun _ _ => idtac).
+  Fail let tac := (fun _ => idtac) in tac.
+  Fail (fun _ => idtac).
+  Fail rec True.
+  Fail let rec tac x := tac in tac True.
+Abort.
\ No newline at end of file
-- 
cgit v1.2.3