From 9723254073261f6c7dd982a6c3e01402cebfa284 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe.lepigre@inria.fr>
Date: Thu, 13 Jun 2019 23:05:54 +0200
Subject: [PATCH] Fix overloaded notation behaviour for offset addition.
---
theories/heap_lang/locations.v | 3 ++-
theories/heap_lang/notation.v | 2 +-
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index dd2a48a3d..b751bc1eb 100644
--- a/theories/heap_lang/locations.v
+++ b/theories/heap_lang/locations.v
@@ -18,7 +18,8 @@ Next Obligation. done. Qed.
Definition loc_add (l : loc) (off : Z) : loc :=
{| loc_car := loc_car l + off|}.
-Notation "l +â‚— off" := (loc_add l off) (at level 50, left associativity).
+Notation "l +â‚— off" :=
+ (loc_add l off) (at level 50, left associativity) : stdpp_scope.
Lemma loc_add_assoc l i j : l +â‚— i +â‚— j = l +â‚— (i + j).
Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index ae3d54943..204ec38ab 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -32,7 +32,7 @@ Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUni
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
-Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
+Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
--
GitLab