From 635ae9c8126dc810d13611b9568d6514d3ebc51c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Aug 2020 18:35:32 +0200
Subject: [PATCH] remove another Coq 8.9 compat hack

---
 theories/algebra/agree.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index e73a3db30..332047646 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -1,7 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import base_logic.
-Import stdpp.list. (* Make sure we use those names. FIXME: remove when we drop Coq 8.9 support. *)
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
-- 
GitLab