Commit 84d73de1 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix issue pointed out by @tchajed in...

Fix issue pointed out by @tchajed in !330 (comment 41322)
parent 260e8ecd
Pipeline #21115 passed with stage
in 16 minutes and 56 seconds
......@@ -220,6 +220,11 @@ Section iris_tests.
iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
eauto.
Qed.
Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
x' x
own γ x - own γ x'.
Proof. intros. by iApply own_mono. Qed.
End iris_tests.
Section monpred_tests.
......
......@@ -70,7 +70,7 @@ Tactic Notation "iStartProof" :=
| |- envs_entails _ _ => idtac
| |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
[iSolveTC || fail "iStartProof: not a BI assertion"
|apply tac_start]
|notypeclasses refine (tac_start _ _)]
end.
(* Same as above, with 2 differences :
......
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