blob: 13efd986f09df1f79b8aab5c026c6769dca9a8fc (
plain)
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
|
Require Import Coq.Program.Tactics.
(** We make a version of [rapply] that takes [uconstr]; we do not
currently test what scope [rapply] interprets terms in. *)
Tactic Notation "urapply" uconstr(p) := rapply p.
Ltac test n :=
(*let __ := match goal with _ => idtac n end in*)
lazymatch n with
| O => let __ := match goal with _ => assert True by urapply I; clear end in
uconstr:(fun _ => I)
| S ?n'
=> let lem := test n' in
let __ := match goal with _ => assert True by (unshelve urapply lem; try exact I); clear end in
uconstr:(fun _ : True => lem)
end.
Goal True.
assert True by urapply I.
assert True by (unshelve urapply (fun _ => I); try exact I).
assert True by (unshelve urapply (fun _ _ => I); try exact I).
assert True by (unshelve urapply (fun _ _ _ => I); try exact I).
clear.
Time let __ := test 50 in idtac.
urapply I.
Qed.
|
