From 49637f62562bf220fc7e2824cea8df134b8731f2 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 17 Aug 2022 10:09:44 -0400 Subject: [PATCH] add Hint Mode for PureExec --- iris/program_logic/language.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v index bcce4c75f..192f9748c 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)). -- GitLab