Add tags in prodn indicating productions that are from plugins,

filtered-only show Ltac2 tags outside of ltac2.rst

1 files changed, 13 insertions, 1 deletions

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;
 }