From 8a9515b04d319bf95dfcc2df777759b6ae577d8f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 14 Dec 2017 15:06:01 +0100
Subject: [PATCH] Fix iStartProof.

---
 theories/proofmode/tactics.v    | 4 ++--
 theories/tests/proofmode_iris.v | 9 +++++++++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index d2172c5d3..9c002eaf9 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -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.
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index ec136a553..f22e3838e 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -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.
-- 
GitLab