From c301e52e1f2bd33077019a2a39d9039cb1e263b4 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 13 Aug 2019 13:15:49 +0200
Subject: [PATCH] Flip cmra_morphism_core

---
 CHANGELOG.md            | 3 ++-
 theories/algebra/cmra.v | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 86a8583a1..35ca2308c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -162,7 +162,8 @@ Changes in Coq:
 * Lemma `prop_ext` works in both directions; its default direction is the
   opposite of what it used to be.
 * Make direction of `f_op` rewrite lemmas more consistent: Flip `pair_op`,
-  `Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`.
+  `Cinl_op`, `Cinr_op`, `cmra_morphism_op`, `cmra_morphism_pcore`,
+  `cmra_morphism_core`.
 * Rename `C` suffixes into `O` since we no longer use COFEs but OFEs. Also
   rename `ofe_fun` into `discrete_fun` and the corresponding notation `-c>` into
   `-d>`. The renaming can be automatically done using the following script (on
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 7d68df52b..714b01afb 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -768,7 +768,7 @@ Qed.
 Section cmra_morphism.
   Local Set Default Proof Using "Type*".
   Context {A B : cmraT} (f : A → B) `{!CmraMorphism f}.
-  Lemma cmra_morphism_core x : core (f x) ≡ f (core x).
+  Lemma cmra_morphism_core x : f (core x) ≡ core (f x).
   Proof. unfold core, core'. rewrite -cmra_morphism_pcore. by destruct (pcore x). Qed.
   Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
   Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
@@ -1597,7 +1597,7 @@ Instance discrete_fun_map_cmra_morphism {A} {B1 B2 : A → ucmraT} (f : ∀ x, B
 Proof.
   split; first apply _.
   - intros n g Hg x; rewrite /discrete_fun_map; apply (cmra_morphism_validN (f _)), Hg.
-  - intros. apply Some_proper=>i. by rewrite (cmra_morphism_core (f i)).
+  - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
   - intros g1 g2 i. by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
 Qed.
 
-- 
GitLab