From a3766213227a4912e1fee2d7ee81c58af8f3452a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 19 Sep 2019 13:40:19 +0200
Subject: [PATCH] Also rename `iPreProp` into `iPrePropO`.
---
tests/algebra.v | 2 +-
theories/base_logic/lib/boxes.v | 2 +-
theories/base_logic/lib/iprop.v | 24 ++++++++++++------------
theories/base_logic/lib/own.v | 4 ++--
theories/base_logic/lib/saved_prop.v | 2 +-
theories/base_logic/lib/wsat.v | 6 +++---
6 files changed, 20 insertions(+), 20 deletions(-)
diff --git a/tests/algebra.v b/tests/algebra.v
index 4fb76957f..b744b8650 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,6 +1,6 @@
From iris.base_logic.lib Require Import invariants.
-Instance test_cofe {Σ} : Cofe (iPreProp Σ) := _.
+Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Section tests.
Context `{!invG Σ}.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 8a89e7935..3e76db385 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -8,7 +8,7 @@ Import uPred.
Class boxG Σ :=
boxG_inG :> inG Σ (prodR
(authR (optionUR (exclR boolO)))
- (optionR (agreeR (laterO (iPreProp Σ))))).
+ (optionR (agreeR (laterO (iPrePropO Σ))))).
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolO)) *
optionRF (agreeRF (▶ ∙)) ) ].
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index cada56389..52f924469 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -116,21 +116,21 @@ Qed.
the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig.
- Parameter iPreProp : gFunctors → ofeT.
- Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ).
+ Parameter iPrePropO : gFunctors → ofeT.
+ Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
Definition iResUR (Σ : gFunctors) : ucmraT :=
- discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
+ discrete_funUR (λ i, gmapUR gname (Σ i (iPrePropO Σ) _)).
Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)).
Notation iPropSI Σ := (uPredSI (iResUR Σ)).
- Parameter iProp_unfold: ∀ {Σ}, iPropO Σ -n> iPreProp Σ.
- Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iPropO Σ.
+ Parameter iProp_unfold: ∀ {Σ}, iPropO Σ -n> iPrePropO Σ.
+ Parameter iProp_fold: ∀ {Σ}, iPrePropO Σ -n> iPropO Σ.
Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
iProp_fold (iProp_unfold P) ≡ P.
- Parameter iProp_unfold_fold: ∀ {Σ} (P : iPreProp Σ),
+ Parameter iProp_unfold_fold: ∀ {Σ} (P : iPrePropO Σ),
iProp_unfold (iProp_fold P) ≡ P.
End iProp_solution_sig.
@@ -138,20 +138,20 @@ Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver.
Definition iProp_result (Σ : gFunctors) :
solution (uPredOF (iResF Σ)) := solver.result _.
- Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
- Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _.
+ Definition iPrePropO (Σ : gFunctors) : ofeT := iProp_result Σ.
+ Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Definition iResUR (Σ : gFunctors) : ucmraT :=
- discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)).
+ discrete_funUR (λ i, gmapUR gname (Σ i (iPrePropO Σ) _)).
Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
- Definition iProp_unfold {Σ} : iPropO Σ -n> iPreProp Σ :=
+ Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ :=
solution_fold (iProp_result Σ).
- Definition iProp_fold {Σ} : iPreProp Σ -n> iPropO Σ := solution_unfold _.
+ Definition iProp_fold {Σ} : iPrePropO Σ -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.
+ Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
Proof. apply solution_fold_unfold. Qed.
End iProp_solution.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 02903ae46..6a37f816f 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -9,10 +9,10 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) :=
- InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) _ }.
+ InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPrePropO Σ) _ }.
Arguments inG_id {_ _} _.
-Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPreProp Σ) _).
+Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPrePropO Σ) _).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index dece3d5aa..7f096f398 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -9,7 +9,7 @@ Import uPred.
saved whatever-you-like. *)
Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
- saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ) _));
+ saved_anything_inG :> inG Σ (agreeR (F (iPrePropO Σ) _));
saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}.
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 1c380e86d..e63dbd9c1 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -9,7 +9,7 @@ exception of what's in the [invG] module. The module [invG] is thus exported in
[fancy_updates], which [wsat] is only imported. *)
Module invG.
Class invG (Σ : gFunctors) : Set := WsatG {
- inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ)))));
+ inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPrePropO Σ)))));
enabled_inG :> inG Σ coPset_disjR;
disabled_inG :> inG Σ (gset_disjR positive);
invariant_name : gname;
@@ -23,7 +23,7 @@ Module invG.
GFunctor (gset_disjUR positive)].
Class invPreG (Σ : gFunctors) : Set := WsatPreG {
- inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ)))));
+ inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPrePropO Σ)))));
enabled_inPreG :> inG Σ coPset_disjR;
disabled_inPreG :> inG Σ (gset_disjR positive);
}.
@@ -33,7 +33,7 @@ Module invG.
End invG.
Import invG.
-Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
+Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPrePropO Σ)) :=
to_agree (Next (iProp_unfold P)).
Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
--
GitLab