From fe17c6af7fee63d0e3b783cb5d965d288d811777 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 26 Oct 2017 17:10:45 +0200
Subject: [PATCH] Put heap_lang's let/lambda/rec at level 200.
Coq also uses level 200 for these constructs.
Besides, heap_lang's match and if were also already at this level.

theories/heap_lang/notation.v  23 +++++++++++
1 file changed, 11 insertions(+), 12 deletions()
diff git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 3263ff157..0ee932730 100644
 a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ 75,10 +75,10 @@ Notation "e1 < e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
(* The breaking point '/ ' makes sure that the body of the rec is indented
by two spaces in case the whole rec does not fit on a single line. *)
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
 (at level 102, f at level 1, x at level 1, e at level 200,
+ (at level 200, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
 (at level 102, f at level 1, x at level 1, e at level 200,
+ (at level 200, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
@@ 88,19 +88,19 @@ are stated explicitly instead of relying on the Notations Let and Seq as
defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
 (at level 102, f, x, y, z at level 1, e at level 200,
+ (at level 200, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
 (at level 102, f, x, y, z at level 1, e at level 200,
+ (at level 200, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : val_scope.
(* The breaking point '/ ' makes sure that the body of the λ: is indented
by two spaces in case the whole λ: does not fit on a single line. *)
Notation "λ: x , e" := (Lam x%bind e%E)
 (at level 102, x at level 1, e at level 200,
+ (at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : expr_scope.
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
 (at level 102, x, y, z at level 1, e at level 200,
+ (at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope.
(* When parsing lambdas, we want them to be locked (so as to avoid needless
@@ 110,21 +110,20 @@ printed too. We achieve that by first defining the nonlocked notation, and then
the locked notation. Both will be used for prettyprinting, but only the last
will be used for parsing. *)
Notation "λ: x , e" := (LamV x%bind e%E)
 (at level 102, x at level 1, e at level 200,
+ (at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x , e" := (locked (LamV x%bind e%E))
 (at level 102, x at level 1, e at level 200,
+ (at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
 (at level 102, x, y, z at level 1, e at level 200,
+ (at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
 (at level 102, x, y, z at level 1, e at level 200,
+ (at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.

Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
 (at level 102, x at level 1, e1, e2 at level 200,
+ (at level 200, x at level 1, e1, e2 at level 200,
format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200,

GitLab