From 3b0c15c3632f9ae670f9140862e159c2776933b5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Nov 2017 19:02:08 +0100
Subject: [PATCH] =?UTF-8?q?Use=20normal=20function=20arrow=20=E2=86=92=20f?=
 =?UTF-8?q?or=20`saved=5Fpred=5Fown`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base_logic/lib/saved_prop.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index ab9e9ba4d..9b5f721e7 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -90,19 +90,20 @@ Qed.
 Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)).
 Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)).
 
-Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -c> iProp Σ) :=
+Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
   saved_anything_own (F := A -c> ▶ ∙) γ (CofeMor Next ∘ Φ).
 
-Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ).
+Instance saved_pred_own_contractive `{savedPredG Σ A} γ :
+  Contractive (saved_pred_own γ : (A -c> iProp Σ) → iProp Σ).
 Proof.
   solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
 Qed.
 
-Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -c> iProp Σ) :
+Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
   (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I.
 Proof. iApply saved_anything_alloc_strong. Qed.
 
-Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A -c> iProp Σ) :
+Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A → iProp Σ) :
   (|==> ∃ γ, saved_pred_own γ Φ)%I.
 Proof. iApply saved_anything_alloc. Qed.
 
-- 
GitLab