diff --git a/theories/simulation/simulation.v b/theories/simulation/simulation.v index 62a639d1b134ba942ab709cf8c9f8e869ce7ccf6..a694ba6c838428a7b0ea074d5a4da2068417f2ae 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.