diff --git a/HeapLang.md b/HeapLang.md
index b9f2cd1125a93051a0cf83671ec31b8d1db55d9b..17c5e144b0200af9cff5dac0c50f3d04df555f18 100644
--- a/HeapLang.md
+++ b/HeapLang.md
@@ -46,6 +46,11 @@ Noteworthy is the fact that functions (`rec:`, `λ:`) in the value scope (`%V`)
 are *locked*.  This is to prevent them from being unfolded and reduced too
 eagerly.
 
+The widely used `#` is a short-hand to turn a basic literal (an integer, a
+location, a boolean literal or a unit value) into a value.  Since values coerce
+to expressions, `#` is widely used whenever a Coq value needs to be placed into
+a HeapLang term.
+
 ## Tactics
 
 HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang