Merge branch 'ci/robbert/issue288' into 'master'

Fix issue #288: iExists fails if goal after the existential quantifier is an evar

Closes #288

See merge request iris/iris!372

tests/proofmode.v

@@ -239,6 +239,17 @@ Proof.
   iFrame.
 Qed.
 
+(* Test for issue #288 *)
+(* FIXME: Restore once we drop support for Coq 8.8 and Coq 8.9.
+Lemma test_iExists_unused : (∃ P : PROP, ∃ x : nat, P)%I.
+Proof.
+  iExists _.
+  iExists 10.
+  iAssert emp%I as "H"; first done.
+  iExact "H".
+Qed.
+*)
+
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.

theories/proofmode/class_instances_bi.v

@@ -4,6 +4,7 @@ From iris.proofmode Require Import base modality_instances classes ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
+(* FIXME(Coq #6294): needs new unification *)
 (** The lemma [from_assumption_exact is not an instance, but defined using
 [notypeclasses refine] through [Hint Extern] to enable the better unification
 algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
@@ -15,6 +16,15 @@ Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
 Hint Extern 0 (FromAssumption _ _ _) =>
   notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
 
+(* FIXME(Coq #6294): needs new unification *)
+(** Similarly, the lemma [from_exist_exist] is defined using a [Hint Extern] to
+enable the better unification algorithm.
+See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
+Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
+Proof. by rewrite /FromExist. Qed.
+Hint Extern 0 (FromExist _ _) =>
+  notypeclasses refine (from_exist_exist _) : typeclass_instances.
+
 Section bi_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
@@ -871,8 +881,6 @@ Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
 Proof. by rewrite /IntoOr -embed_or => <-. Qed.
 
 (** FromExist *)
-Global Instance from_exist_exist {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
-Proof. by rewrite /FromExist. Qed.
 Global Instance from_exist_texist {A} (Φ : tele_arg A → PROP) :
   FromExist (∃.. a, Φ a) Φ.
 Proof. by rewrite /FromExist bi_texist_exist. Qed.