From 35b80feeddb696c1ffa42191f294fca9c06cdb45 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 Aug 2016 21:16:53 +0200
Subject: [PATCH] Make cmra_timeless_included_r consistent with
 cmra_timeless_included_l.

---
 algebra/cmra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 8cec6b6f8..ef47985f9 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -472,8 +472,8 @@ Proof.
   destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
   by exists z'; rewrite Hy (timeless x z).
 Qed.
-Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y.
-Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
+Lemma cmra_timeless_included_r x y : Timeless y → x ≼{0} y → x ≼ y.
+Proof. intros ? [x' ?]. exists x'. by apply (timeless y). Qed.
 Lemma cmra_op_timeless x1 x2 :
   ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
 Proof.
-- 
GitLab