diff options
Diffstat (limited to 'doc/sphinx/language/core/basic.rst')
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 64b29c1c0b..1f0d696d99 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -227,6 +227,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types | @term_match | @term_record | @term_generalizing + | [| {*; @term } %| @term {? : @type } |] {? @univ_annot } | @term_ltac | ( @term ) qualid_annotated ::= @qualid {? @univ_annot } |