`iIntros.` should always enter proof mode
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)