Commit 8a9515b0 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix iStartProof.

parent 8ca83760
......@@ -79,9 +79,9 @@ Proof. rewrite /AsValid=> ->. rewrite bi_embed_valid //. Qed.
Tactic Notation "iStartProof" uconstr(PROP) :=
lazymatch goal with
| |- @envs_entails ?PROP' _ _ =>
let x := type_term (eq_refl : PROP = PROP') in idtac
let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
| |- let _ := _ in _ => fail
| |- ?φ => eapply (@as_valid_2 φ PROP);
| |- ?φ => eapply (λ P : PROP, @as_valid_2 φ _ P);
[apply _ || fail "iStartProof: not a Bi entailment"
|apply tac_adequate]
end.
......
......@@ -36,6 +36,15 @@ Section base_logic_tests.
Lemma test_iAssert_modality P : (|==> False) - |==> P.
Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
Lemma test_iStartProof_1 P : P - P.
Proof. iStartProof. iStartProof. iIntros "$". Qed.
Lemma test_iStartProof_2 P : P - P.
Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
Lemma test_iStartProof_3 P : P - P.
Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
Lemma test_iStartProof_4 P : P - P.
Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
End base_logic_tests.
Section iris_tests.
......
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