diff options
| author | coqbot-app[bot] | 2021-01-28 21:25:59 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-28 21:25:59 +0000 |
| commit | 4ae11ea2bf09fcdf44b1226a45761a2aed34a445 (patch) | |
| tree | f75555ca01275dc1b5331dda71247a04ad141499 /doc/sphinx | |
| parent | ed29e0913742c307175846557ed8390a8da771e3 (diff) | |
| parent | f7d37e69a3df1e049e0bee5d3a58ef2e7cf87af9 (diff) | |
Merge PR #13799: Replace : term with : type in open binders.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 8dbc1626ba..7566996ef6 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -9,7 +9,7 @@ Binders .. insertprodn open_binders binder .. prodn:: - open_binders ::= {+ @name } : @term + open_binders ::= {+ @name } : @type | {+ @binder } name ::= _ | @ident |