Commit 6aa60678 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'trivial-hint-2' into 'master'

Test for !331 and hint for `bi_emp_valid`

See merge request !333
parents 43a77c99 ee17a74d
Pipeline #21064 passed with stage
in 16 minutes and 27 seconds
...@@ -6,6 +6,12 @@ Section tests. ...@@ -6,6 +6,12 @@ Section tests.
Context {PROP : sbi}. Context {PROP : sbi}.
Implicit Types P Q R : PROP. Implicit Types P Q R : PROP.
Lemma test_eauto_emp_isplit_biwand P : emp P - P.
Proof. eauto 6. Qed.
Lemma test_eauto_isplit_biwand P : (P - P)%I.
Proof. eauto. Qed.
Check "demo_0". Check "demo_0".
Lemma demo_0 P Q : (P Q) - ( x, x = 0 x = 1) (Q P). Lemma demo_0 P Q : (P Q) - ( x, x = 0 x = 1) (Q P).
Proof. Proof.
...@@ -158,7 +164,7 @@ Proof. ...@@ -158,7 +164,7 @@ Proof.
iIntros "H". iIntros "H".
let H1 := iFresh in let H1 := iFresh in
let H2 := iFresh in let H2 := iFresh in
let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
iDestruct "H" as pat. iDestruct "H" as pat.
iFrame. iFrame.
Qed. Qed.
......
...@@ -3153,6 +3153,7 @@ Tactic Notation "iAccu" := ...@@ -3153,6 +3153,7 @@ Tactic Notation "iAccu" :=
(** Automation *) (** Automation *)
Hint Extern 0 (_ _) => iStartProof : core. Hint Extern 0 (_ _) => iStartProof : core.
Hint Extern 0 (bi_emp_valid _) => iStartProof : core.
(* Make sure that by and done solve trivial things in proof mode *) (* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core. Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
......
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