aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ltac_missing_args.out
blob: 172612405fa178b5b14bb68c1b229c5379e0b082 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable x.
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable x.
The command has indeed failed with message:
A fully applied tactic is expected: missing arguments for variables y and _.
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable x.
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable x.
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable _.
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable _.
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable _.
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable x.
The command has indeed failed with message:
A fully applied tactic is expected: missing argument for variable x.