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).
---
 test-suite/output/ltac_missing_args.out | 21 +++++++++++++++++++++
 test-suite/output/ltac_missing_args.v   | 19 +++++++++++++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 test-suite/output/ltac_missing_args.out
 create mode 100644 test-suite/output/ltac_missing_args.v

(limited to 'test-suite')

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