blob: 04d7c87c5b76a203658344ee6291babb95660ce6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* The tactic language *)
(* Submitted by Pierre Cr�gut *)
(* Checks substitution of x *)
Tactic Definition f x := Unfold x; Idtac.
Lemma lem1 : (plus O O) = O.
f plus.
Reflexivity.
Qed.
(* Check that Match Context keeps a closure *)
Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a.
Lemma lem2 : True.
U.
Qed.
|
