diff options
| author | Théo Zimmermann | 2020-04-23 22:44:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-23 22:44:33 +0200 |
| commit | ac7996dbd4e6d49d7b5416b27d63b8ce9814f211 (patch) | |
| tree | 49ace6508d87c49169c28e38df3f9c9aef06e343 | |
| parent | c28eaa1067e745ce5b73e7b03162b582e9461a23 (diff) | |
| parent | 29c9d9bd47d5b8cecd6a3ce038cef4302754329f (diff) | |
Merge PR #12154: [documentation] ssreflect: Abbreviations do not support scope
Ack-by: Zimmi48
Reviewed-by: gares
| -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. |