diff options
| author | Pierre-Marie Pédrot | 2017-08-02 18:44:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 18:44:03 +0200 |
| commit | 6e150eb19a55b16bbd4ea03964ee48f2d69084ed (patch) | |
| tree | 99fe2e4afbab5ed8c686ae22f61d22ee01028f79 | |
| parent | 899476fa3dd2ae22f433a70fb860df0510a7ac88 (diff) | |
Typo in documentation.
| -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 ``` |