blob: 541db37fb78ee5f7d15dc9b4f06528820bd5353d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Tactic Notation "test1" open_constr(t) ident(r):=
pose t.
Tactic Notation "test2" constr(r) open_constr(t):=
pose t.
Tactic Notation "test3" open_constr(t) constr(r):=
pose t.
Goal True.
test1 (1 + _) nat.
test2 nat (1 + _).
test3 (1 + _) nat.
test3 (1 + _ : nat) nat.
|
