blob: 40ded54d72b07482b8d42b5a08c7d10d22b52ef3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* 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.
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
|
