1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
(* Test that fresh avoid the variables of intro patterns but also of
simple intro patterns *)
Ltac exploit_main t T pat cleanup
:=
(lazymatch T with
| ?U1 -> ?U2 =>
let H := fresh
in
idtac "H=" H;
assert U1 as H;
[cleanup () | exploit_main (t H) U2 pat ltac:(fun _ => clear H; cleanup ())]
| _ =>
pose proof t as pat;
cleanup ()
end).
Tactic Notation "exploit" constr(t) "as" simple_intropattern(pat)
:=
exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
Goal (True -> True) -> True.
intro H0. exploit H0 as H.
Abort.
Tactic Notation "exploit'" constr(t) "as" intropattern(pat)
:=
exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
Goal (True -> True) -> True.
intro H0. exploit' H0 as H.
Abort.
|
