From 37262a82b917ad82e8ba533d11325fff98cba3c1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 7 Apr 2020 16:24:14 +0200
Subject: [PATCH] fix build on old versions of Coq

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

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 1071f9973..211b5c063 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -1,6 +1,7 @@
 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