From 8834c945fec9cb44af89ebd0a67aabfff4ad9fc6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Mon, 1 Mar 2021 13:54:44 +0900
Subject: [PATCH] fix notation level

---
 theories/lifetime/lifetime_sig.v      | 2 +-
 theories/lifetime/model/definitions.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 5fcb5966..bc2c943b 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -45,7 +45,7 @@ Module Type lifetime_sig.
 
   (** * Notation *)
   Notation "q .[ κ ]" := (lft_tok q κ)
-      (format "q .[ κ ]", at level 0) : bi_scope.
+      (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
   Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
   Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index f1e0adff..b4556a06 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -207,7 +207,7 @@ Instance raw_bor_params : Params (@raw_bor) 4 := {}.
 Instance bor_params : Params (@bor) 4 := {}.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
-    (format "q .[ κ ]", at level 0) : bi_scope.
+    (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
 Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): bi_scope.
 
 Notation "&{ κ }" := (bor κ) (format "&{ κ }") : bi_scope.
-- 
GitLab