From 2e1cc4f5b534895bceb1d2eedde0505faa9ecca0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Dec 2020 18:14:19 +0100
Subject: [PATCH] gmap_view remove duplicate imports, and make sure we export
 the view canonical structure instance

---
 iris/algebra/lib/gmap_view.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 9ea8adff1..c56a8030e 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.
 
-- 
GitLab