diff --git a/tests/tactics/Choose.v b/tests/tactics/Choose.v
index 00cab25f..25b343b6 100644
--- a/tests/tactics/Choose.v
+++ b/tests/tactics/Choose.v
@@ -59,3 +59,13 @@ Goal forall n : nat, ( ( (n = n) \/ (n + 1 = n + 1) ) -> (n + 1 = n + 1)).
     intro n.
     Fail Choose m := n.
 Abort.
+
+(** Test 5: Choose a blank *)
+Goal exists n : nat, n + 1 = n + 1.
+    Choose n := (_).
+Abort.
+
+(** Test 6: Choose a named evar *)
+Goal exists n : nat, n + 1 = n + 1.
+    Choose n := (?[m]).
+Abort.
diff --git a/theories/Tactics/Choose.v b/theories/Tactics/Choose.v
index 7fbb0270..9c58859e 100644
--- a/theories/Tactics/Choose.v
+++ b/theories/Tactics/Choose.v
@@ -22,6 +22,9 @@ Require Import Ltac2.Message.
 Require Import Util.Goals.
 Require Import Util.MessagesToUser.
 
+Local Ltac2 concat_list (ls : message list) : message :=
+  List.fold_right concat (of_string "") ls.
+
 (* Ltac2 Type exn ::= [ ChooseError(string) ]. *)
 
 
@@ -44,9 +47,13 @@ Require Import Util.MessagesToUser.
 Ltac2 choose_variable_in_exists_goal_with_renaming (s:ident) (t:constr) :=
   lazy_match! goal with
     | [ |- exists _ : _, _] =>
-      pose ($s := $t);
+      set ($s := $t);
       let v := Control.hyp s in
       let w := Fresh.fresh (Fresh.Free.of_goal ()) @_defeq in
+      match Constr.has_evar t with
+      |  true => warn (concat_list [of_string "Please come back to this line later to make a definite choice for "; of_ident s; of_string "."])
+      | _ => ()
+      end;
       exists $v;
       assert ($w : $v = $t) by reflexivity
     | [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
@@ -68,14 +75,17 @@ Ltac2 choose_variable_in_exists_goal_with_renaming (s:ident) (t:constr) :=
 *)
 Ltac2 choose_variable_in_exists_no_renaming (t:constr) :=
     lazy_match! goal with
-        | [ |- exists _ : _, _] => exists $t
+        | [ |- exists _ : _, _] =>
+          match Constr.has_evar t with
+          |  true => warn (concat_list [of_string "Please come back to this line later to make a definite choice."]); eexists $t
+          |  false => exists $t
+          end
         | [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
     end.
 
-Ltac2 Notation "Choose" s(opt(seq(ident, ":="))) t(constr) :=
+Ltac2 Notation "Choose" s(opt(seq(ident, ":="))) t(open_constr) :=
   panic_if_goal_wrapped ();
   match s with 
     | None => choose_variable_in_exists_no_renaming t
     | Some s => choose_variable_in_exists_goal_with_renaming s t
   end.
-