From 601625fbb9d2360cb0c858cacfc07df9ac522f3c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 Sep 2019 23:07:17 +0200
Subject: [PATCH] Let `iProp` refer to `uPred ...`, so not the canonical
 structure bundle.

---
 tests/algebra.v                           |  2 +-
 theories/base_logic/lib/iprop.v           | 14 ++++++++------
 theories/base_logic/lib/saved_prop.v      |  6 +++---
 theories/program_logic/total_weakestpre.v |  6 +++---
 theories/program_logic/weakestpre.v       |  4 ++--
 5 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/tests/algebra.v b/tests/algebra.v
index f26776d28..4fb76957f 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -5,7 +5,7 @@ Instance test_cofe {Σ} : Cofe (iPreProp Σ) := _.
 Section tests.
   Context `{!invG Σ}.
 
-  Program Definition test : (iProp Σ -n> iProp Σ) -n> (iProp Σ -n> iProp Σ) :=
+  Program Definition test : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ) :=
     λne P v, (▷ (P v))%I.
   Solve Obligations with solve_proper.
 
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 269b15c9b..cada56389 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -121,12 +121,13 @@ Module Type iProp_solution_sig.
 
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
-  Notation iProp Σ := (uPredO (iResUR Σ)).
+  Notation iProp Σ := (uPred (iResUR Σ)).
+  Notation iPropO Σ := (uPredO (iResUR Σ)).
   Notation iPropI Σ := (uPredI (iResUR Σ)).
   Notation iPropSI Σ := (uPredSI (iResUR Σ)).
 
-  Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
-  Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ.
+  Parameter iProp_unfold: ∀ {Σ}, iPropO Σ -n> iPreProp Σ.
+  Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iPropO Σ.
   Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
     iProp_fold (iProp_unfold P) ≡ P.
   Parameter iProp_unfold_fold: ∀ {Σ} (P : iPreProp Σ),
@@ -142,11 +143,12 @@ Module Export iProp_solution : iProp_solution_sig.
 
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
-  Notation iProp Σ := (uPredO (iResUR Σ)).
+  Notation iProp Σ := (uPred (iResUR Σ)).
+  Notation iPropO Σ := (uPredO (iResUR Σ)).
 
-  Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
+  Definition iProp_unfold {Σ} : iPropO Σ -n> iPreProp Σ :=
     solution_fold (iProp_result Σ).
-  Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
+  Definition iProp_fold {Σ} : iPreProp Σ -n> iPropO Σ := solution_unfold _.
   Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
   Proof. apply solution_unfold_fold. Qed.
   Lemma iProp_unfold_fold {Σ} (P : iPreProp Σ) : iProp_unfold (iProp_fold P) ≡ P.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index af76fb789..dece3d5aa 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -20,14 +20,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
 Proof. solve_inG. Qed.
 
 Definition saved_anything_own `{!savedAnythingG Σ F}
-    (γ : gname) (x : F (iProp Σ) _) : iProp Σ :=
+    (γ : gname) (x : F (iPropO Σ) _) : iProp Σ :=
   own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_anything_own.
 Instance: Params (@saved_anything_own) 4 := {}.
 
 Section saved_anything.
   Context `{!savedAnythingG Σ F}.
-  Implicit Types x y : F (iProp Σ) _.
+  Implicit Types x y : F (iPropO Σ) _.
   Implicit Types γ : gname.
 
   Global Instance saved_anything_persistent γ x :
@@ -106,7 +106,7 @@ Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ)
   saved_anything_own (F := A -d> ▶ ∙) γ (OfeMor Next ∘ Φ).
 
 Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
-  Contractive (saved_pred_own γ : (A -d> iProp Σ) → iProp Σ).
+  Contractive (saved_pred_own γ : (A -d> iPropO Σ) → iProp Σ).
 Proof.
   solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
 Qed.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 920d17d1e..585e3cec2 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -37,8 +37,8 @@ Qed.
 
 (* Uncurry [twp_pre] and equip its type with an OFE structure *)
 Definition twp_pre' `{!irisG Λ Σ} (s : stuckness) :
-  (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) → iProp Σ) →
-  prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) → iProp Σ :=
+  (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ) →
+  prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ :=
     curry3 ∘ twp_pre s ∘ uncurry3.
 
 Local Instance twp_pre_mono' `{!irisG Λ Σ} s : BiMonoPred (twp_pre' s).
@@ -76,7 +76,7 @@ Lemma twp_ind s Ψ :
 Proof.
   iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
   set (Ψ' := curry3 Ψ :
-    prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) → iProp Σ).
+    prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ).
   assert (NonExpansive Ψ').
   { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 36575f35a..4cb5d9161 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -25,8 +25,8 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
 Global Opaque iris_invG.
 
 Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
-    (wp : coPset -d> expr Λ -d> (val Λ -d> iProp Σ) -d> iProp Σ) :
-    coPset -d> expr Λ -d> (val Λ -d> iProp Σ) -d> iProp Σ := λ E e1 Φ,
+    (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
+    coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
   | None => ∀ σ1 κ κs n,
-- 
GitLab