Add tags in prodn indicating productions that are from plugins,

filtered-only show Ltac2 tags outside of ltac2.rst

1 files changed, 3 insertions, 2 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\\}