Merge branch 'pure-exec-mode' into 'master'

add Hint Mode for PureExec See merge request iris/iris!846

Merge branch 'pure-exec-mode' into 'master'
add Hint Mode for PureExec See merge request iris/iris!846
ef762697 · Robbert Krebbers · f7af05e0 · 49637f62 · ef762697
Commit ef762697 authored 2 years ago by Robbert Krebbers
--- 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)).