src/Util/Tactics/PoseTermWithName.v


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.