From 6e150eb19a55b16bbd4ea03964ee48f2d69084ed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 18:44:03 +0200
Subject: Typo in documentation.

---
 doc/ltac2.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/ltac2.md b/doc/ltac2.md
index 20b043ea0b..c2d930c9b6 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -642,7 +642,7 @@ Ltac2 Notation "foo" c(thunk(constr)) ids(list0(ident)) := Bar.f c ids.
 ```
 Then the following expression
 ```
-let y := @X in foo (nat -> nat) x ?y
+let y := @X in foo (nat -> nat) x $y
 ```
 will expand at parsing time to
 ```
-- 
cgit v1.2.3