diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v index bcce4c75f779301e060094582c27797bc6081735..192f9748cbf1424d00e267a09d7d3a73fb8e0eee 100644 --- a/iris/program_logic/language.v +++ b/iris/program_logic/language.v @@ -327,6 +327,8 @@ Section language. End language. +Global Hint Mode PureExec + - - ! - : typeclass_instances. + Global Arguments step_atomic {Λ Ï1 κ Ï2}. Notation pure_steps_tp := (Forall2 (rtc pure_step)).