From f8dee71f42ed1034adf6b28d76f7f742af0003e7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Feb 2021 12:39:19 +0100
Subject: [PATCH] more implicit Arguments for step_atomic

---
 iris/program_logic/language.v       | 2 ++
 iris/program_logic/total_adequacy.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index 98f3e685f..280a6d36b 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -328,4 +328,6 @@ Section language.
 
 End language.
 
+Global Arguments step_atomic {Λ ρ1 κ ρ2}.
+
 Notation pure_steps_tp := (Forall2 (rtc pure_step)).
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 1e9554680..a717aa570 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -67,7 +67,7 @@ Proof.
   apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
   - destruct t as [|e1' ?]; simplify_eq/=.
     + iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)".
-      { by eapply (step_atomic _ _ _ _ _ _ _ _ []). }
+      { by eapply (step_atomic _ _ _ _ _ []). }
       iModIntro. iExists n2. iFrame "Hσ".
       rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
       by setoid_rewrite (right_id_L [] (++)).
-- 
GitLab