From e18882f01022c801a3bfffed99f3dcd7982e2a5d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Feb 2016 23:59:19 +0100
Subject: [PATCH] Missing heap_lang let: notation for values.

---
 heap_lang/notation.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 161f33f18..c235428c5 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -52,6 +52,8 @@ Notation "λ: x , e" := (LamV x e%L)
   (at level 102, x at level 1, e at level 200) : lang_scope.
 Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
   (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
+Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L)
+  (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
 Notation "e1 ;; e2" := (Lam "" e2%L e1%L)
   (at level 100, e2 at level 200) : lang_scope.
 
-- 
GitLab