From e4975c8bc7175cff660222a271e52d58b6efcc45 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 31 Jul 2017 19:52:52 +0200
Subject: [PATCH] Put the shift_loc notation in the right scope so that it is
 parsed/printed properly even when appearing in expressions.

---
 theories/lang/lang.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 14520ff7..b7abe7f6 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -198,7 +198,8 @@ Definition lit_of_bool (b : bool) : base_lit :=
 
 Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
 
-Notation "l +â‚— z" := (shift_loc l%L z%Z) (at level 50, left associativity).
+Notation "l +â‚— z" := (shift_loc l%L z%Z)
+  (at level 50, left associativity) : loc_scope.
 
 Fixpoint init_mem (l:loc) (init:list val) (σ:state) : state :=
   match init with
-- 
GitLab