diff options
| author | Erik Martin-Dorel | 2019-03-01 00:06:08 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-03-01 00:06:08 +0100 |
| commit | c5156ef960467334fb5ae38dfd5a8740115ee09b (patch) | |
| tree | 4473303622771ed6852ed229e2f19f0ffe11af5a /doc | |
| parent | 8b42c73a6a3b417e848952e7510e27d74e6e1758 (diff) | |
[doc] ssr: Fix the documentation of `by [tacs]`
Closes coq/coq#9669
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 237b534d67..b81830f06b 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2094,9 +2094,9 @@ into a closing one (similar to :tacn:`now`). Its general syntax is: :name: by :undocumented: -The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to -:n:`[by @tactic | by @tactic | ...]` and this form should be preferred -to the former. +The Ltac expression :n:`by [@tactic | @tactic | …]` is equivalent to +:n:`do [done | by @tactic | by @tactic | …]`, which corresponds to the +standard Ltac expression :n:`first [done | @tactic; done | @tactic; done | …]`. In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed |