Commit ee17a74d authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso

Add another missing hint

parent 0f5eca67
......@@ -10,7 +10,7 @@ Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
Proof. eauto 6. Qed.
Lemma test_eauto_isplit_biwand P : (P - P)%I.
Proof. iStartProof. eauto. Qed.
Proof. eauto. Qed.
Check "demo_0".
Lemma demo_0 P Q : (P Q) - ( x, x = 0 x = 1) (Q P).
......
......@@ -3153,6 +3153,7 @@ Tactic Notation "iAccu" :=
(** Automation *)
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 *)
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