Commit 84481877 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add [] spec patterns for missing premises of iApply.

This fixes issue #51.
parent 3d46bb4d
...@@ -426,13 +426,14 @@ Tactic Notation "iApply" open_constr(lem) := ...@@ -426,13 +426,14 @@ Tactic Notation "iApply" open_constr(lem) :=
| ITrm ?t ?xs ?pat => constr:(ITrm t xs ("*" +:+ pat)) | ITrm ?t ?xs ?pat => constr:(ITrm t xs ("*" +:+ pat))
| _ => constr:(ITrm lem hnil "*") | _ => constr:(ITrm lem hnil "*")
end in end in
iPoseProofCore lem as false true (fun H => first let rec go H := first
[iExact H [eapply tac_apply with _ H _ _ _;
|eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity [env_cbv; reflexivity
|let P := match goal with |- IntoWand ?P _ _ => P end in |apply _
apply _ || fail 1 "iApply: cannot apply" P |lazy beta (* reduce betas created by instantiation *)]
|lazy beta (* reduce betas created by instantiation *)]]). |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)]).
(** * Revert *) (** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) := Local Tactic Notation "iForallRevert" ident(x) :=
......
...@@ -116,3 +116,7 @@ Proof. ...@@ -116,3 +116,7 @@ Proof.
iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". } iAssert True%I with "[HP]" as %_. { Fail iClear "HQ". by iClear "HP". }
done. done.
Qed. Qed.
Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
(P - Q - True - True - 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