From e60b556f1cfadf163025d400fa6bf41ac0b625b0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 May 2018 16:22:15 +0200
Subject: [PATCH] bump std++, use the new [default] notation

---
 opam                             | 2 +-
 theories/algebra/cmra.v          | 2 +-
 theories/algebra/coPset.v        | 2 +-
 theories/algebra/gmultiset.v     | 2 +-
 theories/algebra/gset.v          | 2 +-
 theories/algebra/list.v          | 4 ++--
 theories/algebra/ofe.v           | 2 +-
 theories/bi/tactics.v            | 4 ++--
 theories/proofmode/classes.v     | 4 ++--
 theories/proofmode/coq_tactics.v | 2 +-
 10 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/opam b/opam
index e8c09aef1..8d54dbbb1 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.9~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2018-05-24.0.de797b31") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-05-29.0.4014c929") | (= "dev") }
 ]
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b22018df5..d5fa7ff44 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -179,7 +179,7 @@ Class Core (A : Type) := core : A → A.
 Hint Mode Core ! : typeclass_instances.
 Instance: Params (@core) 2.
 
-Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
+Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
 Arguments core' _ _ _ /.
 
 (** * CMRAs with a unit element *)
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 653043cdf..763ca1e29 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -46,7 +46,7 @@ Section coPset.
   Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed.
   Canonical Structure coPsetUR := UcmraT coPset coPset_ucmra_mixin.
 
-  Lemma coPset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
+  Lemma coPset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
 
   Lemma coPset_update X Y : X ~~> Y.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index c3bcfa600..612620318 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -55,7 +55,7 @@ Section gmultiset.
     apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X ∪)).
   Qed.
 
-  Lemma gmultiset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
+  Lemma gmultiset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
 
   Lemma gmultiset_update X Y : X ~~> Y.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 15555f385..b4d5e520d 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -45,7 +45,7 @@ Section gset.
   Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
   Canonical Structure gsetUR := UcmraT (gset K) gset_ucmra_mixin.
 
-  Lemma gset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
+  Lemma gset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
 
   Lemma gset_update X Y : X ~~> Y.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index ec603646c..1f20a1592 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -56,7 +56,7 @@ Canonical Structure listC := OfeT (list A) list_ofe_mixin.
 
 Program Definition list_chain
     (c : chain listC) (x : A) (k : nat) : chain A :=
-  {| chain_car n := from_option id x (c n !! k) |}.
+  {| chain_car n := default x (c n !! k) |}.
 Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
 Definition list_compl `{Cofe A} : Compl listC := λ c,
   match c 0 with
@@ -354,7 +354,7 @@ Section properties.
     x ~~>: P → (∀ y, P y → Q [y]) → [x] ~~>: Q.
   Proof.
     rewrite !cmra_total_updateP=> Hup HQ n lf /list_lookup_validN Hv.
-    destruct (Hup n (from_option id ε (lf !! 0))) as (y&?&Hv').
+    destruct (Hup n (default ε (lf !! 0))) as (y&?&Hv').
     { move: (Hv 0). by destruct lf; rewrite /= ?right_id. }
     exists [y]; split; first by auto.
     apply list_lookup_validN=> i.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index a291eea0c..4eb180241 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -905,7 +905,7 @@ Section option.
   Canonical Structure optionC := OfeT (option A) option_ofe_mixin.
 
   Program Definition option_chain (c : chain optionC) (x : A) : chain A :=
-    {| chain_car n := from_option id x (c n) |}.
+    {| chain_car n := default x (c n) |}.
   Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
   Definition option_compl `{Cofe A} : Compl optionC := λ c,
     match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
diff --git a/theories/bi/tactics.v b/theories/bi/tactics.v
index 6c6794868..8674be924 100644
--- a/theories/bi/tactics.v
+++ b/theories/bi/tactics.v
@@ -13,7 +13,7 @@ Module bi_reflection. Section bi_reflection.
   Fixpoint eval (Σ : list PROP) (e : expr) : PROP :=
     match e with
     | EEmp => emp
-    | EVar n => from_option id emp (Σ !! n)
+    | EVar n => default emp (Σ !! n)
     | ESep e1 e2 => eval Σ e1 ∗ eval Σ e2
     end%I.
   Fixpoint flatten (e : expr) : list nat :=
@@ -23,7 +23,7 @@ Module bi_reflection. Section bi_reflection.
     | ESep e1 e2 => flatten e1 ++ flatten e2
     end.
 
-  Notation eval_list Σ l := ([∗ list] n ∈ l, from_option id emp (Σ !! n))%I.
+  Notation eval_list Σ l := ([∗ list] n ∈ l, default emp (Σ !! n))%I.
 
   Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
   Proof.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 3ead29d0f..9d94d8cff 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -526,7 +526,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
     instances to recognize the [emp] case and make it look nicer. *)
 Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
            (α β : X → PROP) (mγ : X → option PROP) : PROP :=
-  M1 (∃ x, α x ∗ (β x -∗ M2 (from_option id emp (mγ x))))%I.
+  M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
 
 (* Typeclass for assertions around which accessors can be elliminated.
    Inputs: [Q], [E1], [E2], [α], [β], [γ]
@@ -582,7 +582,7 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
 Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
       (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
       (Q : PROP) (Q' : X → PROP) :=
-  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (from_option id (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
+  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
 Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
 Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
 Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 8ea775935..79a6599b9 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -445,7 +445,7 @@ Proof.
 Qed.
 
 Lemma maybe_wand_sound (mP : option PROP) Q :
-  maybe_wand mP Q ⊣⊢ (from_option id emp mP -∗ Q).
+  maybe_wand mP Q ⊣⊢ (default emp mP -∗ Q).
 Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
 
 Global Instance envs_Forall2_refl (R : relation PROP) :
-- 
GitLab