From 39a10cba3d610c6f12438084c5de7c1217c8fe94 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 15 Jun 2018 11:44:32 +0200 Subject: Checking if low-level name printers are used on purpose or not. In particular we check if really used for internal debugging purpose or to display a message to the user. In the latter case, we replace it (when possible) by a higher-level printer (e.g. printing foo instead of Top.foo). In the former case, we clarify that the use is a debugging use. Still not perfect (see a few FIXME). --- test-suite/output/ltac_missing_args.out | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'test-suite') diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 7326f137c2..8a00cd3fe5 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,25 +1,25 @@ The command has indeed failed with message: -The user-defined tactic "Top.foo" was not fully applied: +The user-defined tactic "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: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "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: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "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: -The user-defined tactic "Top.baz" was not fully applied: +The user-defined tactic "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: -The user-defined tactic "Top.qux" was not fully applied: +The user-defined tactic "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: -The user-defined tactic "Top.mydo" was not fully applied: +The user-defined tactic "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: @@ -31,7 +31,7 @@ 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: -The user-defined tactic "Top.rec" was not fully applied: +The user-defined tactic "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: -- cgit v1.2.3