2 files changed, 65 insertions, 6 deletions
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
index 3548b8754c..3dfe4db439 100644
--- a/doc/sphinx/_static/coqnotations.sty
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -67,11 +67,26 @@
 
 \newcssclass{notation-sup}{\nsup{#1}}
 \newcssclass{notation-sub}{\nsub{#1}}
-\newcssclass{notation}{\nnotation{#1}}
+\newcssclass{notation}{\nnotation{\textbf{#1}}}
 \newcssclass{repeat}{\nrepeat{#1}}
 \newcssclass{repeat-wrapper}{\nwrapper{#1}}
+\newcssclass{repeat-wrapper-with-sub}{\nwrapper{#1}}
 \newcssclass{hole}{\nhole{#1}}
 \newcssclass{alternative}{\nalternative{\nbox{#1}}{0pt}}
 \newcssclass{alternative-block}{#1}
 \newcssclass{repeated-alternative}{\nalternative{#1}{\nboxsep}}
 \newcssclass{alternative-separator}{\quad\naltsep{}\quad}
+\newcssclass{prodn-table}{%
+  \begin{savenotes}
+  \sphinxattablestart
+  \begin{tabulary}{\linewidth}[t]{lLL}
+  #1
+  \end{tabulary}
+  \par
+  \sphinxattableend
+  \end{savenotes}}
+% latex puts targets 1 line below where they should be; prodn-target corrects for this
+\newcssclass{prodn-target}{\raisebox{\dimexpr \nscriptsize \relax}{#1}}
+\newcssclass{prodn-cell-nonterminal}{#1 &}
+\newcssclass{prodn-cell-op}{#1 &}
+\newcssclass{prodn-cell-production}{#1\\}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 4a5fa0b328..3806ba6ee6 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -10,6 +10,7 @@
 .notation {
     /* font-family: "Ubuntu Mono", "Consolas", monospace; */
     white-space: pre-wrap;
+    font-weight: bold;
 }
 
 .notation .notation-sup {
@@ -85,7 +86,8 @@
     padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
 }
 
-.notation .repeat-wrapper {
+.notation .repeat-wrapper,
+.notation .repeat-wrapper-with-sub {
     display: inline-block;
     position: relative;
     margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */
@@ -165,10 +167,52 @@
 /* Overrides */
 /*************/
 
-.rst-content table.docutils td, .rst-content table.docutils th {
-    padding: 8px; /* Reduce horizontal padding */
-    border-left: none;
-    border-right: none;
+.prodn-table {
+    display: table;
+    margin: 1.5em 0px;
+    vertical-align: baseline;
+    font-weight: bold;
+}
+
+.prodn-column-group  {
+    display: table-column-group;
+}
+
+.prodn-column {
+    display: table-column;
+}
+
+.prodn-row-group {
+    display: table-row-group;
+}
+
+.prodn-row {
+    display: table-row;
+}
+
+.prodn-cell-nonterminal,
+.prodn-cell-op,
+.prodn-cell-production
+{
+    display: table-cell;
+}
+
+.prodn-cell-nonterminal {
+    padding-right: 0.49em;
+}
+
+.prodn-cell-op {
+    padding-right: 0.90em;
+    font-weight: normal;
+}
+
+.prodn-table .notation > .repeat-wrapper {
+    margin-top: 0.28em;
+}
+
+.prodn-table .notation > .repeat-wrapper-with-sub {
+    margin-top: 0.28em;
+    margin-bottom: 0.28em;
 }
 
 /* We can't display nested blocks otherwise */