summaryrefslogtreecommitdiff
path: root/test-suite/output/ltac_extra_args.out
blob: 77e799d35936ce1320aa2d16f33576f780cafc02 (plain)
1
2
3
4
5
6
7
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.