From aa9b972ee3b0f8166ef69e4dfd97082e863d5441 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Aug 2016 15:23:32 +0200
Subject: [PATCH] No longer use later_car in the logic.

It is not non-expansive, so not a function we should use.
---
 algebra/cofe.v             | 2 --
 algebra/upred.v            | 3 +--
 program_logic/ownership.v  | 2 +-
 program_logic/saved_prop.v | 2 +-
 4 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index 0d35a88a0..9742a0915 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -675,8 +675,6 @@ Inductive later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
 Arguments Next {_} _.
 Arguments later_car {_} _.
-Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
-Proof. by destruct x. Qed.
 
 Section later.
   Context {A : cofeT}.
diff --git a/algebra/upred.v b/algebra/upred.v
index 37cc9c626..781094a60 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1213,8 +1213,7 @@ Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by unseal. Qed.
 
 (* Later *)
-Lemma later_equivI {A : cofeT} (x y : later A) :
-  x ≡ y ⊣⊢ ▷ (later_car x ≡ later_car y).
+Lemma later_equivI {A : cofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
 Proof. by unseal. Qed.
 
 (* Discrete *)
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index ad1ae6176..f59c7af6f 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -126,7 +126,7 @@ Proof.
     iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI.
     iRewrite -"HvI" in "HI". by rewrite agree_idemp. }
   rewrite /invariant_unfold.
-  by rewrite agree_equivI uPred.later_equivI /= iProp_unfold_equivI.
+  by rewrite agree_equivI uPred.later_equivI iProp_unfold_equivI.
 Qed.
 
 Lemma ownI_open i P : wsat ★ ownI i P ★ ownE {[i]} ⊢ wsat ★ ▷ P ★ ownD {[i]}.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 0874a7e9f..ecfe85db2 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -35,7 +35,7 @@ Section saved_prop.
   Lemma saved_prop_agree γ x y :
     saved_prop_own γ x ★ saved_prop_own γ y ⊢ ▷ (x ≡ y).
   Proof.
-    rewrite -own_op own_valid agree_validI agree_equivI later_equivI /=.
+    rewrite -own_op own_valid agree_validI agree_equivI 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