diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/_static/ansi.css | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/repl/ansicolors.py | 5 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 1 |
5 files changed, 6 insertions, 5 deletions
diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css index 2a618f68d2..a4850a738b 100644 --- a/doc/sphinx/_static/ansi.css +++ b/doc/sphinx/_static/ansi.css @@ -69,7 +69,7 @@ } .ansi-fg-white { - color: #2e3436; + color: #ffffff; } .ansi-fg-light-black { diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 9f097b4fe9..abe928fa26 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -5,7 +5,7 @@ The underlying formal language of Coq is a :gdef:`Calculus of Inductive Constructions` (|Cic|) whose inference rules are presented in this chapter. The history of this formalism as well as pointers to related -work are provided in a separate chapter; see *Credits*. +work are provided in a separate chapter; see :ref:`history`. .. _The-terms: diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py index 9e23be2409..6700c20b1a 100644 --- a/doc/tools/coqrst/repl/ansicolors.py +++ b/doc/tools/coqrst/repl/ansicolors.py @@ -91,7 +91,10 @@ def parse_ansi(code): leading ‘^[[’ or the final ‘m’ """ classes = [] - parse_style([int(c) for c in code.split(';')], 0, classes) + if code == "37": + pass # ignore white fg + else: + parse_style([int(c) for c in code.split(';')], 0, classes) return ["ansi-" + cls for cls in classes] if __name__ == '__main__': diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index ab1a9d4c75..0c8980b1bd 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1778,7 +1778,6 @@ simple_tactic: [ | "zify_iter_let" tactic (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string "in" ident (* ring plugin *) | "protect_fv" string (* ring plugin *) | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5b19b7fc55..40bb980e90 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1856,7 +1856,6 @@ simple_tactic: [ | "zify_iter_let" ltac_expr (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" one_term (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string OPT ( "in" ident ) | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) |