From d755c546a5c260232fd30971bd604b078d0afc18 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 17:31:13 +0200
Subject: Properly implementing the notation to easily access hypotheses.

---
 doc/ltac2.md | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/ltac2.md b/doc/ltac2.md
index 12687e9aff..bf6d9eb583 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -470,8 +470,12 @@ as follows.
 constr:(fun x : nat => ltac2:(exact (hyp @x)))
 ```
 
-The `ltac2:(exact (hyp @x))` pattern is so common that we provide dedicated
-Ltac2 and Coq term notations for it.
+This pattern is so common that we provide dedicated Ltac2 and Coq term notations
+for it.
+
+- `&x` as an Ltac2 expression expands to `hyp @x`.
+- `&x` as an Coq constr expression expands to
+  `ltac2:(refine (fun () => hyp @x))`.
 
 #### Dynamic semantics
 
-- 
cgit v1.2.3