diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v index 295fe6a8ae4a721aa94c92f818932ebd0c09eb3d..cfc7e1b414219ac438a9bd6645efa7a941c44f57 100644 --- a/theories/heap_lang/adequacy.v +++ b/theories/heap_lang/adequacy.v @@ -1,4 +1,4 @@ -From iris.program_logic Require Export weakestpre adequacy gen_heap. +From iris.program_logic Require Export weakestpre adequacy. From iris.heap_lang Require Export lifting. From iris.algebra Require Import auth. From iris.heap_lang Require Import proofmode notation.