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

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

2 files changed, 16 insertions, 3 deletions

diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
index 3dfe4db439..2b1678e7ef 100644
--- a/doc/sphinx/_static/coqnotations.sty
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -79,7 +79,7 @@
 \newcssclass{prodn-table}{%
   \begin{savenotes}
   \sphinxattablestart
-  \begin{tabulary}{\linewidth}[t]{lLL}
+  \begin{tabulary}{\linewidth}[t]{lLLL}
   #1
   \end{tabulary}
   \par
@@ -89,4 +89,5 @@
 \newcssclass{prodn-target}{\raisebox{\dimexpr \nscriptsize \relax}{#1}}
 \newcssclass{prodn-cell-nonterminal}{#1 &}
 \newcssclass{prodn-cell-op}{#1 &}
-\newcssclass{prodn-cell-production}{#1\\}
+\newcssclass{prodn-cell-production}{#1 &}
+\newcssclass{prodn-cell-tag}{#1\\}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 9546f7107e..8c3f7ac3c1 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -192,7 +192,8 @@
 
 .prodn-cell-nonterminal,
 .prodn-cell-op,
-.prodn-cell-production
+.prodn-cell-production,
+.prodn-cell-tag
 {
     display: table-cell;
 }
@@ -206,6 +207,17 @@
     font-weight: normal;
 }
 
+.prodn-cell-production {
+    width: 99%;
+}
+
+.prodn-cell-tag {
+    text-align: right;
+    font-weight: normal;
+    font-size: 75%;
+    font-family: "Lato","proxima-nova","Helvetica Neue",Arial,sans-serif;
+}
+
 .prodn-table .notation > .repeat-wrapper {
     margin-top: 0.28em;
 }