From b588e825699b873686daa7ab0f7bfb99bc8347da Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 10 Jun 2021 19:42:27 +0200
Subject: [PATCH] make sim_ectx simpl never

---
 theories/simulation/simulation.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/simulation/simulation.v b/theories/simulation/simulation.v
index 62a639d1..a694ba6c 100644
--- a/theories/simulation/simulation.v
+++ b/theories/simulation/simulation.v
@@ -80,3 +80,6 @@ Section fix_lang.
   Definition sim_expr_ectx `{!SimE s} π K_t K_s Φ :=
     (∀ v_t v_s, ext_rel π v_t v_s -∗ sim_expr Φ π (fill K_t (of_val v_t)) (fill K_s (of_val v_s)))%I.
 End fix_lang.
+
+Global Arguments sim_ectx : simpl never.
+Global Arguments sim_expr_ectx : simpl never.
-- 
GitLab