1 files changed, 10 insertions, 0 deletions
diff --git a/src/Util/Tactics/PoseTermWithName.v b/src/Util/Tactics/PoseTermWithName.v
new file mode 100644
index 000000000..3dba9a211
--- /dev/null
+++ b/src/Util/Tactics/PoseTermWithName.v
@@ -0,0 +1,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.