From ffd67c0926c2d9ddaa881b087b128dcf7a40b2b1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 30 Jun 2018 00:01:34 +0200
Subject: [PATCH] bind scope before defining notation, to make sure the scope
is set for the notation
---
tests/heap_lang.v | 2 ++
theories/heap_lang/lang.v | 8 ++++----
2 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index eba3026da..54d46b46e 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -19,6 +19,8 @@ Section tests.
end.
Qed.
+ Definition val_scope_test_1 := SOMEV (#(), #()).
+
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 4a98fbbe8..41ebd16fb 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -66,11 +66,11 @@ Inductive expr :=
| CAS (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr).
+Bind Scope expr_scope with expr.
+
Notation NONE := (InjL (Lit LitUnit)) (only parsing).
Notation SOME x := (InjR x) (only parsing).
-Bind Scope expr_scope with expr.
-
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Var x => bool_decide (x ∈ X)
@@ -97,11 +97,11 @@ Inductive val :=
| InjLV (v : val)
| InjRV (v : val).
+Bind Scope val_scope with val.
+
Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
Notation SOMEV x := (InjRV x) (only parsing).
-Bind Scope val_scope with val.
-
Fixpoint of_val (v : val) : expr :=
match v with
| RecV f x e => Rec f x e
--
GitLab