Commit da56bbb0 authored by Robbert Krebbers's avatar Robbert Krebbers

Unused premises go to the last premise of iApply (instead of the first).

parent 4d3e8866
......@@ -17,8 +17,8 @@ Applying hypotheses and lemmas
conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
proof mode terms below.
If the applied term has more premises than given specialization patterns, the
pattern is extended with `[-] ... [-]`. As a consequence, all unused spatial
hypotheses move to the first premise without an explicit specialization
pattern is extended with `[] ... []`. As a consequence, all unused spatial
hypotheses move to the last premise without an explicit specialization
pattern.
Context management
......
......@@ -431,7 +431,7 @@ Tactic Notation "iApply" open_constr(lem) :=
[env_cbv; reflexivity
|apply _
|lazy beta (* reduce betas created by instantiation *)]
|iSpecializePat H "[-]"; last go H] in
|iSpecializePat H "[]"; last go H] in
iPoseProofCore lem as false true (fun H =>
first [iExact H|go H|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
......
......@@ -118,5 +118,5 @@ Proof.
Qed.
Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
(P - Q - True - True - R) - P - Q - R.
(P - True - True - Q - R) - P - Q - R.
Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.
Markdown is supported
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