From b9390e6935425421c596a819f967bd26fa7ab576 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 May 2020 21:21:20 +0200
Subject: [PATCH] Remove `Local` that is incompatible with Coq 8.9.

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

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index ea78bca9c..7b153697c 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -16,7 +16,7 @@ Section bi_mixin.
   Context (bi_wand : PROP â†’ PROP â†’ PROP).
   Context (bi_persistently : PROP â†’ PROP).
 
-  Local Bind Scope bi_scope with PROP.
+  Bind Scope bi_scope with PROP.
   Local Infix "âŠ¢" := bi_entails.
   Local Notation "'emp'" := bi_emp : bi_scope.
   Local Notation "'True'" := (bi_pure True) : bi_scope.
-- 
GitLab