diff options
| -rw-r--r-- | doc/ltac2.md | 2 |
1 files changed, 1 insertions, 1 deletions
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 ``` |