From 4077176318a24d5d349384873bc6297a93a89fc2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Feb 2016 03:06:20 +0100
Subject: [PATCH] Remove some left-over junk.

---
 algebra/fin_maps.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index c54e70b0d..49aad3300 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -288,10 +288,6 @@ End freshness.
 
 (* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]},
    then the frame could always own "unit x", and prevent deallocation. *)
-(*
-Lemma option_fmap_op {B : cmraT} (f : A → B) (mx my : option A) : f <$> mx ⋅ my = (f <$> mx) ⋅ (f <$> my).
-Proof. destruct mx, my; simpl; try done.
-*)
 Global Instance map_alter_update `{!LocalUpdate P f} i :
   LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ P x) (alter f i).
 Proof.
-- 
GitLab