diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v index 9ea8adff174f391b6f38a4a261f06e8e5901e50e..c56a8030e8fca592aff6b11fe2741d7f1e23ef06 100644 --- a/iris/algebra/lib/gmap_view.v +++ b/iris/algebra/lib/gmap_view.v @@ -1,6 +1,5 @@ From Coq.QArith Require Import Qcanon. -From iris.algebra Require Import view updates dfrac. -From iris.algebra Require Export gmap dfrac. +From iris.algebra Require Export view gmap dfrac. From iris.algebra Require Import local_updates proofmode_classes. From iris.prelude Require Import options.