diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:49:20 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:49:20 +0100 |
| commit | 6551e32184c508ca9894422e4bc523043049145e (patch) | |
| tree | e19168e580bb4d378e64ae4156bdc65c6aed7c7e /test-suite/output | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
| parent | ee79408adfd058a098388b98d24c893178c7a0c4 (diff) | |
Merge PR #6210: More complete not-fully-applied error messages, #6145
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/ltac_missing_args.out | 40 |
1 files changed, 30 insertions, 10 deletions
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 172612405..7326f137c 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. |