Merge branch 'robbert/iApply_pretty' into 'master'

Fix bug in `iApply` prettification.

See merge request !788

iris/proofmode/ltac_tactics.v

@@ -1240,8 +1240,7 @@ Local Ltac iApplyHypLoop H :=
     [eapply tac_apply with H _ _ _;
       [pm_reflexivity
       |iSolveTC
-      |pm_reduce;
-       pm_prettify (* reduce redexes created by instantiation *)]
+      |pm_reduce]
     |iSpecializePat H "[]"; last iApplyHypLoop H].
 
 Tactic Notation "iApplyHyp" constr(H) :=
@@ -1253,7 +1252,9 @@ Tactic Notation "iApplyHyp" constr(H) :=
      end].
 
 Tactic Notation "iApply" open_constr(lem) :=
-  iPoseProofCore lem as false (fun H => iApplyHyp H).
+  iPoseProofCore lem as false (fun H => iApplyHyp H);
+  pm_prettify. (* reduce redexes created by instantiation; this is done at the
+  very end after all type classes have been solved. *)
 
 (** * Disjunction *)
 Tactic Notation "iLeft" :=

tests/proofmode.ref

@@ -385,6 +385,18 @@ No applicable tactic.
   "HP" : default emp mP
   --------------------------------------∗
   default emp mP
+"test_iApply_prettification3"
+     : string
+1 goal
+  
+  PROP : bi
+  Ψ, Φ : nat → PROP
+  HP : ∀ (f : nat → nat) (y : nat),
+         TCEq f (λ x : nat, x + 10) → Ψ (f 1) -∗ Φ y
+  ============================
+  "H" : Ψ 11
+  --------------------------------------∗
+  Ψ (1 + 10)
 1 goal
   
   PROP : bi

tests/proofmode.v

@@ -1109,6 +1109,17 @@ Proof.
   iIntros "?". iExists _. iApply modal_if_lemma2. done.
 Qed.
 
+Check "test_iApply_prettification3".
+Lemma test_iApply_prettification3 (Ψ Φ : nat → PROP) :
+  (∀ f y, TCEq f (λ x, x + 10) → Ψ (f 1) -∗ Φ y) →
+  Ψ 11 -∗ Φ 10.
+Proof.
+  iIntros (HP) "H".
+  iApply HP. (* should be [Ψ (1 + 10)], without a beta redex *)
+  Show.
+  iApply "H".
+Qed.
+
 Lemma test_iDestruct_clear P Q R :
   P -∗ (Q ∗ R) -∗ True.
 Proof.