Skip to content

Fix bug in `iApply` prettification.

Robbert Krebbers requested to merge robbert/iApply_pretty into master

Situation before this MR:

From iris.proofmode Require Import tactics.

Lemma test_iApply_reduce {PROP : bi} (Ψ Φ : nat  PROP) :
  ( f y, TCEq f (λ x, x + 10)  Ψ (f 1) -∗ Φ y) 
  Ψ 11 -∗ Φ 10.
Proof.
  iIntros (HP) "H".
  iApply HP. (* [Ψ ((λ x : nat, x + 10) 1)] does not reduce *)
  reduction.pm_reduce. (* [Ψ (1 + 10)] does reduce *)
Restart.
  iIntros (HP) "H".
  iApply (HP _ _ _). (* [Ψ (1 + 10)] does reduce *) 
  iApply "H".
Qed.

This MR fixes this problem by moving the pm_prettify to the outside. This is needed because only at that moment all TCs have been solved.

Edited by Robbert Krebbers

Merge request reports