Commit 854dcaaf authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 3121e4ed
Pipeline #65345 passed with stage
in 10 minutes and 14 seconds
......@@ -1115,7 +1115,7 @@ Lemma test_iApply_prettification3 (Ψ Φ : nat → PROP) :
Ψ 11 - Φ 10.
Proof.
iIntros (HP) "H".
iApply HP.
iApply HP. (* should be [Ψ (1 + 10)], without a beta redex *)
Show.
iApply "H".
Qed.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment