Test with merge_sbi branch of Iris.

.gitlab-ci.yml

@@ -27,19 +27,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.11.0:
+build-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.11.0"
+    OPAM_PINS: "coq version 8.11.0   coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#ci/robbert/merge_sbi"
   tags:
   - fp-timing
 
-build-iris.dev:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV  coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
-  except:
-  only:
-  - triggers
-  - schedules
-  - api

theories/bi/fracpred.v

@@ -150,10 +150,7 @@ Module Import fracPred.
   Ltac unseal :=
     unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp, bi_and, bi_or,
            bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
-           bi_persistently, bi_affinely, sbi_later;
-    simpl;
-    unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
-           sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently;
+           bi_persistently, bi_affinely, sbi_later, sbi_internal_eq;
     simpl;
     rewrite !unseal_eqs /=.
 End fracPred.
@@ -220,9 +217,6 @@ Proof.
     rewrite left_id_L bi.pure_True // left_id. by apply bi.persistently_and_sep_elim.
 Qed.
 
-Canonical Structure fracPredI (PROP : bi) : bi :=
-  {| bi_ofe_mixin := fracPred_ofe_mixin; bi_bi_mixin := fracPred_bi_mixin PROP |}.
-
 Lemma fracPred_sbi_mixin (PROP : sbi) :
   SbiMixin (PROP:=fracPred PROP) fracPred_entails fracPred_pure
            fracPred_or fracPred_impl fracPred_forall fracPred_exist
@@ -260,10 +254,12 @@ Proof.
   - intros P. split=> π /=. apply bi.later_false_em.
 Qed.
 
-Canonical Structure fracPredSI (PROP: sbi) : sbi :=
-  {| sbi_ofe_mixin := fracPred_ofe_mixin; sbi_bi_mixin := fracPred_bi_mixin PROP;
+Canonical Structure fracPredI (PROP : bi) : bi :=
+  {| bi_ofe_mixin := fracPred_ofe_mixin; bi_bi_mixin := fracPred_bi_mixin PROP;
      sbi_sbi_mixin := fracPred_sbi_mixin PROP |}.
 
+Notation fracPredSI := fracPredI.
+
 Class FObjective {PROP : bi} (P : fracPred PROP) :=
   fobjective_at π π' : P π -∗ P π'.
 Arguments FObjective {_} _%I.