diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v index 76ae35bf4240b69d9e8e1f44b0cbb203a96b9ef6..8c6da6f5b725a53ff722fdfdc970d0386a790d5b 100644 --- a/theories/program_logic/adequacy.v +++ b/theories/program_logic/adequacy.v @@ -1,4 +1,3 @@ -From stdpp Require Import namespaces. From iris.program_logic Require Export weakestpre. From iris.algebra Require Import gmap auth agree gset coPset. From iris.base_logic.lib Require Import wsat.