iExists fails if goal after the existential quantifier is an evar
Iris version: dev.2019-11-22.2.a979391c
iExists
fails if you have a goal of the form
∃ _, ?P
Here is a test case which illustrates the problem:
Lemma test Σ:
(∃ P, ∃ (_ : True), P : iProp Σ)%I.
Proof.
iExists _.
(* Here iExists fails *)
Fail iExists _.
(* Solving the existential quantifier manually *)
eapply coq_tactics.tac_exist.
(* Using apply fails *)
Fail apply @class_instances_bi.from_exist_exist.
(* But apply: works *)
apply: @class_instances_bi.from_exist_exist. simpl.
eexists _.
Abort.