From fc77fc3a44ab5a7fe17bf9f81ad5af77c27134b8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 5 Oct 2016 13:08:31 +0200
Subject: [PATCH] Fix the lemma Some_included' for total CMRAs.

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

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 474b1af41..79a64561a 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1208,8 +1208,8 @@ Section option.
 
   Lemma Some_included x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
   Proof. rewrite option_included; naive_solver. Qed.
-  Lemma Some_included' `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
-  Proof. rewrite Some_included; naive_solver. Qed.
+  Lemma Some_included' `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≼ y.
+  Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed.
   Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my.
   Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
 End option.
-- 
GitLab