From a9f986035259b41fc256aa45eafcae8ea0585041 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 5 Oct 2018 14:14:04 +0200
Subject: [PATCH] Use only printing on notations for lambdas.

---
 theories/heap_lang/notation.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index f8ef7a585..80e876e8c 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -114,18 +114,17 @@ Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
 (* When parsing lambdas, we want them to be locked (so as to avoid needless
 unfolding by tactics and unification). However, unlocked lambda-values sometimes
 appear as part of compound expressions, in which case we want them to be pretty
-printed too. We achieve that by first defining the non-locked notation, and then
-the locked notation. Both will be used for pretty-printing, but only the last
-will be used for parsing. *)
+printed too. We achieve that by using printing only notations for the non-locked
+notation. *)
 Notation "λ: x , e" := (LamV x%bind e%E)
   (at level 200, x at level 1, e at level 200,
-   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
+   format "'[' 'λ:'  x ,  '/  ' e ']'", only printing) : val_scope.
 Notation "λ: x , e" := (locked (LamV x%bind e%E))
   (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 200, x, y, z at level 1, e at level 200,
-   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'", only printing) : val_scope.
 Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
   (at level 200, x, y, z at level 1, e at level 200,
    format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
-- 
GitLab