blob: 3dba9a211e607269a47e20baf67e11e0e7f7a864 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Ltac pose_term_with tac name :=
let name := fresh name in
let v := tac () in
let dummy := match goal with
| _ => pose v as name
end in
name.
Ltac pose_term_with_type type tac name :=
pose_term_with ltac:(fun u => let v := tac u in constr:(v : type)) name.
|