diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v index 179eac0fc705603bb9133a2a5613c9ca1a92be39..104146e5375cb8407374ea47fe79085f2edffc1b 100644 --- a/theories/base_logic/lib/fractional.v +++ b/theories/base_logic/lib/fractional.v @@ -1,5 +1,5 @@ From stdpp Require Import gmap gmultiset. -From iris.base_logic Require Export derived. +From iris.base_logic Require Export base_logic. From iris.base_logic Require Import big_op. From iris.proofmode Require Import classes class_instances. Set Default Proof Using "Type".