From 4a7e39323bd57ac41ec90d4ea18f10423029e8b5 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 12 Apr 2020 11:40:28 -0700
Subject: Convert ltac2 chapter to use prodn, update syntax

---
 doc/sphinx/language/core/basic.rst | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/sphinx/language/core/basic.rst')

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 }
-- 
cgit v1.2.3