diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v index 5a947722e037588d984dc0986e66116d8885bc44..4aecb160d51b6889c2eda280322030a7d07b3b24 100644 --- a/theories/base_logic/base_logic.v +++ b/theories/base_logic/base_logic.v @@ -1,6 +1,5 @@ From iris.base_logic Require Export derived. From iris.bi Require Export bi. -From iris.proofmode Require Import tactics. From iris.algebra Require Import proofmode_classes. Set Default Proof Using "Type".