diff options
| author | Pierre-Marie Pédrot | 2018-03-13 17:13:48 +0100 |
|---|---|---|
| committer | GitHub | 2018-03-13 17:13:48 +0100 |
| commit | 797cd88b4ea91780fca394a12044f9613ed63fc6 (patch) | |
| tree | 4007d544304358c9d99f85d797fd3da997beaf85 | |
| parent | 7f0a281f3b15d76213475316b7d18d8c37fc6f96 (diff) | |
| parent | 7dbf6dbd73f3a828bbb58458191912f895cf7779 (diff) | |
Merge pull request coq/ltac2#49 from Armael/fix-typo
Fix a typo
| -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 cd0d8f4325..10a65fce44 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -875,7 +875,7 @@ Due to conflicts, a few syntactic rules have changed. `try`, `repeat`, `do`, `once`, `progress`, `time`, `abstract`. - `idtac` is no more. Either use `()` if you expect nothing to happen, `(fun () => ())` if you want a thunk (see next section), or use printing - primitives from the `Message` module if you wand to display something. + primitives from the `Message` module if you want to display something. ## Tactic delay |