diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v index 749685bb20297e011844ded7cb923cc27afb6d00..8fe8c536f01f18157b74cfdaeb8052261a725ba5 100644 --- a/iris/base_logic/upred.v +++ b/iris/base_logic/upred.v @@ -1,4 +1,3 @@ -From stdpp Require Import finite. From iris.algebra Require Export cmra updates. From iris.bi Require Import notation. From iris.prelude Require Import options.