diff options
| author | Maxime Dénès | 2019-05-23 16:40:05 +0200 |
|---|---|---|
| committer | GitHub | 2019-05-23 16:40:05 +0200 |
| commit | 15891b8179a82884bf72df8c7d7d696d29f53434 (patch) | |
| tree | f54f342364e2ce17036187c1223a803a9b0da789 | |
| parent | f08df3055c110a3ae5b708a384fe681e170dfbba (diff) | |
Update doc/sphinx/user-extensions/syntax-extensions.rst
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 70c41d5be0..06259e4db0 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1173,7 +1173,7 @@ Binding types of arguments to an interpretation scope Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). .. note:: When active, a bound scope has effect on all defined functions - (even if they are defined after the `Bind Scope` directive), except + (even if they are defined after the :cmd:`Bind Scope` directive), except if argument scopes were assigned explicitly using the :cmd:`Arguments <Arguments (scopes)>` command. |