From 40898af40c428611718d51c8aef8d53defe53b99 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Jun 2021 12:05:57 +0200
Subject: [PATCH] Disambiguate an fmap.

Follow up of e1c5e026df5862647322cf2e8a3c3d56f434ab19
---
 iris_staging/heap_lang/interpreter.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris_staging/heap_lang/interpreter.v b/iris_staging/heap_lang/interpreter.v
index 36b2f4b9b..2e773ca47 100644
--- a/iris_staging/heap_lang/interpreter.v
+++ b/iris_staging/heap_lang/interpreter.v
@@ -151,7 +151,7 @@ Module interp_monad.
   Proof. by inversion 1. Qed.
 
   Lemma mret_inv {A} (v: A) s v' s' :
-    mret (M := InterpretM) v s = (inl v', s') → v = v' ∧ s = s'.
+    mret (M:=InterpretM) v s = (inl v', s') → v = v' ∧ s = s'.
   Proof. by inversion 1. Qed.
 
   Lemma interp_bind_inv A B (x: InterpretM A) (f: A → InterpretM B) r s s' :
@@ -176,7 +176,7 @@ Module interp_monad.
   Qed.
 
   Lemma interp_fmap_inv {A B} (f: A → B) x s v s' :
-    (f <$> x) s = (inl v, s') →
+    (fmap (M:=InterpretM) f x) s = (inl v, s') →
     ∃ v0, v = f v0 ∧ x s = (inl v0, s').
   Proof.
     rewrite /fmap /interp_fmap.
-- 
GitLab