From 30fc910b01f61ce3691ed63a0908c1c60cee76dd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 16:46:29 +0200
Subject: Fix documentation.

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

diff --git a/doc/ltac2.md b/doc/ltac2.md
index fee19e5df0..7a3b2181f8 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -467,11 +467,11 @@ Rather, the tactic writer has to resort to the **dynamic** goal environment,
 and must write instead explicitly that she is accessing a hypothesis, typically
 as follows.
 ```
-constr:(fun x : nat => ltac2:(hyp @x))
+constr:(fun x : nat => ltac2:(exact (hyp @x)))
 ```
 
-The `ltac2:(hyp @x)` pattern is so common that we provide a dedicated Coq
-term notation for it.
+The `ltac2:(exact (hyp @x))` pattern is so common that we provide dedicated
+Ltac2 and Coq term notations for it.
 
 #### Dynamic semantics
 
-- 
cgit v1.2.3