diff options
| author | Maxime Dénès | 2017-03-17 09:08:36 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-17 09:08:36 +0100 |
| commit | b317c77e7b40ebf2558d298fddfce4f6997afc5c (patch) | |
| tree | 633ab3fa6c6409ca1ef4e8d296a45214b4142653 /test-suite | |
| parent | ac3ee8cba2d27f2be38ba706e49aeee08086d936 (diff) | |
| parent | 028db341f3cb924c2d1b3a9e0fa5666425130f90 (diff) | |
Merge PR#428: Report missing tactic arguments in error message
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/ltac_missing_args.out | 21 | ||||
| -rw-r--r-- | test-suite/output/ltac_missing_args.v | 19 |
2 files changed, 40 insertions, 0 deletions
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 |