From 47f304f6552fb15cd3aaeba5feb7183ad571d2d2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 10 Jun 2019 18:35:02 +0200
Subject: [PATCH] fix build with Coq 8.10 and newer

---
 theories/algebra/namespace_map.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index aaaae3bf8..94789d0f1 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -67,7 +67,7 @@ Canonical Structure namespace_mapC :=
 
 Global Instance NamespaceMap_discrete a b :
   Discrete a → Discrete b → Discrete (NamespaceMap a b).
-Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
+Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
 Global Instance namespace_map_ofe_discrete :
   OfeDiscrete A → OfeDiscrete namespace_mapC.
 Proof. intros ? [??]; apply _. Qed.
-- 
GitLab