From 3121e4edfb4d09e6a9bec8b4bd2f0a400d9f44e0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Apr 2022 21:37:19 +0200
Subject: [PATCH] Fix bug in `iApply` prettification.

---
 iris/proofmode/ltac_tactics.v |  7 ++++---
 tests/proofmode.ref           | 12 ++++++++++++
 tests/proofmode.v             | 11 +++++++++++
 3 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index f4da0ed78..380e71fa9 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/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" :=
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ce21d1c9d..9a7ac3b30 100644
--- a/tests/proofmode.ref
+++ b/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
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8ad3f6da4..d67a8b9d1 100644
--- a/tests/proofmode.v
+++ b/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.
+  Show.
+  iApply "H".
+Qed.
+
 Lemma test_iDestruct_clear P Q R :
   P -∗ (Q ∗ R) -∗ True.
 Proof.
-- 
GitLab