From eddf607bd32e4c1399f1feb948fa103f1010513e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Apr 2020 22:38:46 +0200
Subject: [PATCH] =?UTF-8?q?Make=20use=20of=20`=E2=96=B7^`=20notation=20in?=
 =?UTF-8?q?=20its=20definition.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This works because there is already a `Reserved Notation`.
---
 theories/bi/derived_connectives.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 8576c1525..28488c4fa 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -86,11 +86,11 @@ Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
 Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
   match n with
   | O => P
-  | S n' => â–· sbi_laterN n' P
-  end%I.
+  | S n' => â–· â–·^n' P
+  end%I
+where "â–·^ n P" := (sbi_laterN n P) : bi_scope.
 Arguments sbi_laterN {_} !_%nat_scope _%I.
 Instance: Params (@sbi_laterN) 2 := {}.
-Notation "â–·^ n P" := (sbi_laterN n P) : bi_scope.
 Notation "â–·? p P" := (sbi_laterN (Nat.b2n p) P) : bi_scope.
 
 Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
-- 
GitLab