aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/coqrst
AgeCommit message (Collapse)Author
2021-04-19Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in ↵coqbot-app[bot]
Sphinx output Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2021-04-17Include (* ... *) comments in .. coqtop:: directives in Sphinx outputJim Fehrle
2021-04-17Remove superfluous sort.Jim Fehrle
Removing it makes no difference to the order of glossary entries, which is determined by the "for ... sorted" statement above.
2021-04-10Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on ↵coqbot-app[bot]
red/orange background) Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2021-03-12Fixed grammar productions for PDF documentationsIsaac Oscar Gariano
This undoes changes by 48bb58156acec84991a9e570e93a4e31c0349e79 that broke the rendering of grammar productions in PDfs.
2021-03-04Correctly sort the glossaryJim Fehrle
2021-02-14Show "Error:"/"Warning:" with white type (on red/orange background)Jim Fehrle
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-26Set the locale in Docker so Python's default output encoding is utf-8Jim Fehrle
2020-12-16Add -q flag to coqrst python invocation of coqtopLasse Blaauwbroek
This will help with reproducibility for people who have something in their coqrc file. Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-09Allow any character in a tacn, cmd, ... nameJim Fehrle
Include "0-9_" in default cmd name Report duplicate names
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-09-18Fix Removed in Sphinx 4 deprecations.Théo Zimmermann
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-11Remove outdated references to productionlist.Théo Zimmermann
2020-07-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
filtered-only show Ltac2 tags outside of ltac2.rst
2020-06-09Merge PR #12103: Convert Ltac chapter to prodnThéo Zimmermann
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
- by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except - don't generate a name for cmdv and tacv - generate more flexibily for exn, warn and attr
2020-06-07[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_linesClément Pit-Claudel
2020-06-07Merge PR #12473: Match only a single line as the coqtop prompt in coqtop:: ↵Clément Pit-Claudel
directive
2020-06-06Match only a single line as the coqtop promptJim Fehrle
(the previous expression was including some expected output)
2020-06-05Fix comment.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Remove note about Sphinx tradition.
2020-06-05[sphinx] Fix #12361Clément Pit-Claudel
2020-06-05[sphinx] Improve the error message printed for duplicate namesClément Pit-Claudel
2020-06-05[sphinx] Remove most pylint warningsClément Pit-Claudel
2020-05-18Support :gdef:`text <term>` syntax (adding "<term>")Jim Fehrle
2020-05-11Checking validity of coqdoc file name.Hugo Herbelin
This fixes #12265 (javascript injection vulnerability in file name).
2020-05-08Recursively look for the first string nodeQuentin Carbonneaux
2020-05-08Simplify splittingQuentin Carbonneaux
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-04-29Support in-line glossary entries and referencesJim Fehrle
with an index
2020-04-19Don't create index entries for the name "_"Jim Fehrle
2020-04-02Merge PR #11869: Add an index for attributes.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-22Format hyperlink targets and link ids with the same nameJim Fehrle
(translate '_' to '-' consistently)
2020-03-20Add an index for attributes.Théo Zimmermann
2020-03-19[refman] Stop using the deprecated math_block node (fixed GH-11856)Clément Pit-Claudel
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-09Remove some productionlistsJim Fehrle
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-26Addr 'attr' directive for attributesJim Fehrle
2020-02-24Allow multiple indexed names on a single .. cmd::, etc.Jim Fehrle
2020-02-17Merge PR #11614: Show apostrophes and backticks in HTML doc, too.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-16Show apostrophes and backticks in HTML, too.Jim Fehrle
2020-02-13Spell out the entry suffix in the main indexJim Fehrle
Ex: "(tactic)" instead of "(tacn)"
2020-01-27checkdeps.py: report *all* missing dependencies at oncePaolo G. Giarrusso
Otherwise you need a few feedback loops to install all dependencies.
2020-01-27checkdeps: check for sphinxcontrib-bibtexPaolo G. Giarrusso
I lacked this package, and got: ``` $ make -j2 COQ_USE_DUNE=1 refman-html [...] env doc/sphinx_build (exit 2) (cd _build/default/doc && /usr/bin/env COQLIB=.. sphinx-build -j4 -W -b html -d sphinx_build/doctrees sphinx sphinx_build/html) Running Sphinx v2.1.2 Extension error: Could not import extension sphinxcontrib.bibtex (exception: No module named 'sphinxcontrib.bibtex') make: *** [refman-html] Error 1 ```
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:56:00 +0000