diff options
| author | Kenji Maillard | 2020-04-22 15:35:22 +0200 |
|---|---|---|
| committer | Kenji Maillard | 2020-04-23 19:41:11 +0200 |
| commit | 29c9d9bd47d5b8cecd6a3ce038cef4302754329f (patch) | |
| tree | 8f7c415c50886ec716f225891f75bc673b3a3692 | |
| parent | 0c4775fcb48207c96752b81c76f67c17e5fd3c99 (diff) | |
[documentation] ssreflect: Abbreviations do not support scope
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b5d1e8bffd..28c5359a04 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1624,9 +1624,15 @@ previous :token:`i_item` have been performed. The second entry in the :token:`i_view` grammar rule, ``/ltac:(`` :token:`tactic` ``)``, executes :token:`tactic`. -Notations can be used to name tactics, for example:: +Notations can be used to name tactics, for example - Notation myop := (ltac:(some ltac code)) : ssripat_scope. +.. coqtop:: none + + Tactic Notation "my" "ltac" "code" := idtac. + +.. coqtop:: in warn + + Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope. lets one write just ``/myop`` in the intro pattern. Note the scope annotation: views are interpreted opening the ``ssripat`` scope. |