diff options
| author | Jim Fehrle | 2020-10-11 18:39:16 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-27 12:15:35 -0700 |
| commit | b402adc12c00ba72046423d3a1737ccad517f70e (patch) | |
| tree | 1940efc064bf87b9b996a0e21eaa75e9b57605d4 /doc/sphinx | |
| parent | 5f5cddae48c08872107f30938dcc2f3c8d91f33a (diff) | |
Rename operconstr -> term
Diffstat (limited to 'doc/sphinx')
| -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 0c51361b64..94a705a4c6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -510,7 +510,7 @@ Displaying information about notations The output for `Print Grammar constr` includes :cmd:`Notation` definitions, which are dynamically added to the grammar at run time. - For example, in the definition for `operconstr`, the production on the second line shown + For example, in the definition for `term`, the production on the second line shown here is defined by a :cmd:`Reserved Notation` command in `Notations.v`:: | "50" LEFTA |