From 13dc3369e4f31e455d53c8227ecceee8d50ebb09 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Aug 2017 21:41:58 +0200
Subject: [PATCH] Explicitly unfold some definitions.

These unfolds kind of make sense, and I was quite surprised that
it used to work before. However, when changing to primitive
records, these unfolds are actually needed.
---
 theories/base_logic/lib/cancelable_invariants.v | 2 +-
 theories/base_logic/lib/gen_heap.v              | 4 ++--
 theories/base_logic/lib/saved_prop.v            | 3 ++-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index b85789b5a..9d5f84d7f 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -39,7 +39,7 @@ Section proofs.
   Proof. rewrite /cinv; apply _. Qed.
 
   Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
-  Proof. intros ??. by rewrite -own_op. Qed.
+  Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
   Global Instance cinv_own_as_fractionnal γ q :
     AsFractional (cinv_own γ q) (cinv_own γ) q.
   Proof. split. done. apply _. Qed.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index c851970e9..a0ac009cf 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -87,7 +87,7 @@ Section gen_heap.
   Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
-    intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
+    intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
       op_singleton pair_op agree_idemp.
   Qed.
   Global Instance mapsto_as_fractional l q v :
@@ -97,7 +97,7 @@ Section gen_heap.
   Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     apply wand_intro_r.
-    rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
     f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
     by intros [_ ?%agree_op_invL'].
   Qed.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 6bc0bda63..4ab1fd029 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -37,7 +37,8 @@ Section saved_prop.
     saved_prop_own γ x -∗ saved_prop_own γ y -∗ ▷ (x ≡ y).
   Proof.
     apply wand_intro_r.
-    rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
+    rewrite /saved_prop_own -own_op own_valid agree_validI agree_equivI.
+    rewrite later_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.
-- 
GitLab