From e1c5e026df5862647322cf2e8a3c3d56f434ab19 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Jun 2021 11:17:46 +0200
Subject: [PATCH] disambiguate an mret

Thanks to Paolo G. Giarrusso
---
 iris_staging/heap_lang/interpreter.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris_staging/heap_lang/interpreter.v b/iris_staging/heap_lang/interpreter.v
index 8d7e31a97..36b2f4b9b 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 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' :
-- 
GitLab