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.
---
 test-suite/output/ltac_extra_args.out |  8 ++++++++
 test-suite/output/ltac_extra_args.v   | 10 ++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 test-suite/output/ltac_extra_args.out
 create mode 100644 test-suite/output/ltac_extra_args.v

(limited to 'test-suite')

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