blob: 01bf727ebc8df05732634924fa6da9b699447d5a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Ltac f H := split; [ a H | e H ]
Ltac g := match goal with
| |- context [ if ?X then _ else _ ] => case X
end
The command has indeed failed with message:
H is already used.
The command has indeed failed with message:
H is already used.
a
The command has indeed failed with message:
This variable is used in hypothesis H.
Ltac test a b c d e := apply a, b in c as [], d, e as ->
|
