Merge PR #12085: Convert ltac2 chapter to use prodn, update syntax

Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Ack-by: ppedrot

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 }