From d52fc2766ac00255a2440995bfa58d8febf06237 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 18 Dec 2017 20:09:05 +0100
Subject: [PATCH] Add some tests.

---
 _CoqProject                        |  1 +
 theories/tests/proofmode_monPred.v | 30 ++++++++++++++++++++++++++++++
 2 files changed, 31 insertions(+)
 create mode 100644 theories/tests/proofmode_monPred.v

diff --git a/_CoqProject b/_CoqProject
index f467b8c0a..e3a98170f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -97,6 +97,7 @@ theories/tests/heap_lang.v
 theories/tests/one_shot.v
 theories/tests/proofmode.v
 theories/tests/proofmode_iris.v
+theories/tests/proofmode_monPred.v
 theories/tests/list_reverse.v
 theories/tests/tree_sum.v
 theories/tests/ipm_paper.v
diff --git a/theories/tests/proofmode_monPred.v b/theories/tests/proofmode_monPred.v
new file mode 100644
index 000000000..e9f2053ea
--- /dev/null
+++ b/theories/tests/proofmode_monPred.v
@@ -0,0 +1,30 @@
+From iris.proofmode Require Import tactics monpred.
+From iris.base_logic Require Import base_logic lib.invariants.
+
+Section tests.
+  Context {I : bi_index} {PROP : sbi}.
+  Local Notation monPred := (monPred I PROP).
+  Local Notation monPredI := (monPredI I PROP).
+  Local Notation monPredSI := (monPredSI I PROP).
+  Implicit Types P Q R : monPred.
+  Implicit Types i j : I.
+
+  Lemma test0 P : P -∗ P.
+  Proof. iIntros "$". Qed.
+
+  Lemma test_iStartProof_1 P : P -∗ P.
+  Proof. iStartProof. iStartProof. iIntros "$". Qed.
+  Lemma test_iStartProof_2 P : P -∗ P.
+  Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
+  Lemma test_iStartProof_3 P : P -∗ P.
+  Proof. iStartProof monPredI. iStartProof monPredSI. iIntros "$". Qed.
+  Lemma test_iStartProof_4 P : P -∗ P.
+  Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
+  Lemma test_iStartProof_5 P : P -∗ P.
+  Proof. iStartProof PROP. iIntros (i) "$". Qed.
+  Lemma test_iStartProof_6 P : P ⊣⊢ P.
+  Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
+  Lemma test_iStartProof_7 P : ((P ≡ P)%I : monPredI).
+  Proof. iStartProof PROP. done. Qed.
+
+End tests.
\ No newline at end of file
-- 
GitLab