diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v index 6f3f155c3904460fda7ddad836aa72ee83f12a2c..547cb57f46e7b02f4ea22cc45468099a8df08309 100644 --- a/theories/heap_lang/proph_erasure.v +++ b/theories/heap_lang/proph_erasure.v @@ -1,5 +1,5 @@ -From iris.heap_lang Require Export lang notation tactics. From iris.program_logic Require Export adequacy. +From iris.heap_lang Require Export lang notation tactics. (** This file contains the proof that prophecies can be safely erased from programs. We erase a program by replacing prophecy identifiers