From 94640742cb785744d3c20269eeadd7fef93275f3 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 3 Nov 2020 14:11:07 -0600
Subject: [PATCH] Remove unneeded changes to gmap_view
---
theories/algebra/lib/gmap_view.v | 14 +++++++-------
1 file changed, 7 insertions(+), 7 deletions(-)
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 9a5449b1b..5439678fe 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -298,11 +298,11 @@ Section lemmas.
{ destruct (bf !! k) as [[df' va']|] eqn:Hbf; last done.
specialize (Hrel _ _ Hbf). destruct Hrel as (v' & _ & _ & Hm).
exfalso. rewrite Hm in Hfresh. done. }
- rewrite lookup_singleton Hbf right_id_L.
+ rewrite lookup_singleton Hbf right_id.
intros [= <- <-]. eexists. do 2 (split; first done).
rewrite lookup_insert. done.
- rewrite lookup_singleton_ne; last done.
- rewrite left_id_L=>Hbf.
+ rewrite left_id=>Hbf.
specialize (Hrel _ _ Hbf). destruct Hrel as (v' & ? & ? & Hm).
eexists. do 2 (split; first done).
rewrite lookup_insert_ne //.
@@ -336,14 +336,14 @@ Section lemmas.
rewrite Hbf. clear Hbf.
rewrite -Some_op -pair_op.
move=>[/= /dfrac_full_exclusive Hdf _]. done. }
- rewrite Hbf right_id_L lookup_singleton. clear Hbf.
+ rewrite Hbf right_id lookup_singleton. clear Hbf.
intros [= <- <-].
eexists. do 2 (split; first done).
rewrite lookup_insert. done.
- rewrite lookup_singleton_ne; last done.
- rewrite left_id_L=>Hbf.
+ rewrite left_id=>Hbf.
edestruct (Hrel j) as (v'' & ? & ? & Hm).
- { rewrite lookup_op lookup_singleton_ne // left_id_L. done. }
+ { rewrite lookup_op lookup_singleton_ne // left_id. done. }
simpl in *. eexists. do 2 (split; first done).
rewrite lookup_insert_ne //.
Qed.
@@ -367,9 +367,9 @@ Section lemmas.
apply cmra_discrete_valid_iff. done.
+ simpl in *. move:Hbf=>[= <- <-]. split; done.
- rewrite lookup_singleton_ne //.
- rewrite left_id_L=>Hbf.
+ rewrite left_id=>Hbf.
edestruct (Hrel j) as (v'' & ? & ? & Hm).
- { rewrite lookup_op lookup_singleton_ne // left_id_L. done. }
+ { rewrite lookup_op lookup_singleton_ne // left_id. done. }
simpl in *. eexists. do 2 (split; first done). done.
Qed.
--
GitLab