diff options
Diffstat (limited to 'doc/sphinx/proof-engine/ltac.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index c5ee724ca..2b128b98f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -245,7 +245,7 @@ focused goals with: :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested - in a tactic expression, by using the keyword :tacn:`only`: + in a tactic expression, by using the keyword ``only``: .. tacv:: only selector : expr :name: only ... : ... @@ -826,6 +826,7 @@ We can make pattern matching on goals using the following expression: .. we should provide the full grammar here .. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i=1,...,m\ :sub:`1` is matched (non-linear first-order unification) by an hypothesis of the |