From cf265ef5e32f08562db702fb545fb5d346e0e924 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 21 Sep 2017 18:36:00 -0400
Subject: Report missing arguments in error message

Augment the "Illegal tactic application" error message with the number
of extra arguments passed.

Fixes BZ#5753.
---
 plugins/ltac/tacinterp.ml             |  8 +++++++-
 test-suite/output/ltac_extra_args.out |  8 ++++++++
 test-suite/output/ltac_extra_args.v   | 10 ++++++++++
 3 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/output/ltac_extra_args.out
 create mode 100644 test-suite/output/ltac_extra_args.v

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 8fa95ffb02..3a8526874d 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 *)
diff --git a/test-suite/output/ltac_extra_args.out b/test-suite/output/ltac_extra_args.out
new file mode 100644
index 0000000000..77e799d359
--- /dev/null
+++ b/test-suite/output/ltac_extra_args.out
@@ -0,0 +1,8 @@
+The command has indeed failed with message:
+Illegal tactic application: got 1 extra argument.
+The command has indeed failed with message:
+Illegal tactic application: got 2 extra arguments.
+The command has indeed failed with message:
+Illegal tactic application: got 1 extra argument.
+The command has indeed failed with message:
+Illegal tactic application: got 2 extra arguments.
diff --git a/test-suite/output/ltac_extra_args.v b/test-suite/output/ltac_extra_args.v
new file mode 100644
index 0000000000..4caf619fee
--- /dev/null
+++ b/test-suite/output/ltac_extra_args.v
@@ -0,0 +1,10 @@
+Ltac foo := idtac.
+Ltac bar H := idtac.
+
+Goal True.
+Proof.
+  Fail foo H.
+  Fail foo H H'.
+  Fail bar H H'.
+  Fail bar H H' H''.
+Abort.
-- 
cgit v1.2.3