aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Expand)Author
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-08Recursively look for the first string nodeQuentin Carbonneaux
2020-05-08Simplify splittingQuentin Carbonneaux
2020-05-07Cleanup formatting in .. coqtop:: directivesQuentin Carbonneaux
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-29Merge PR #12150: Support in-line glossary definitions and references with an ...Clément Pit-Claudel
2020-04-29Support in-line glossary entries and referencesJim Fehrle
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-21Update common.edit_mlg and fullGrammar following #12038.Théo Zimmermann
2020-04-19Don't create index entries for the name "_"Jim Fehrle
2020-04-13Update syntax of Import / Export in documentation.Théo Zimmermann
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10Suppress the space after "#" when printing productionsJim Fehrle
2020-04-10Ignore subscripts in notation for matching cmds and tacsJim Fehrle
2020-04-10Fix prefix matchingJim Fehrle
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
2020-04-02Merge PR #11869: Add an index for attributes.Clément Pit-Claudel
2020-03-30[dune] [docgram] Remove bash hack thanks to new option -no-update.Théo Zimmermann
2020-03-30Merge PR #11958: Add -no-update command line option to doc_grammar for DuneThéo Zimmermann
2020-03-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
2020-03-29Merge PR #11938: Support for updating orderedGrammar with Dune.Emilio Jesus Gallego Arias
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Update fullGrammar and orderedGrammar following #11877.Théo Zimmermann
2020-03-28New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.Théo Zimmermann
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-22Format hyperlink targets and link ids with the same nameJim Fehrle
2020-03-20Add an index for attributes.Théo Zimmermann
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
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-19Update fullGrammar, common.edit_mlg and orderedGrammar...Théo Zimmermann
2020-03-19Update fullGrammar and common.edit_mlg following #11839.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-12Dune build rules for doc_grammar and fullGrammar.Théo Zimmermann
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-24Add OPTREF and INSERTALL editing operationsJim Fehrle
2020-02-24Generate prodnCommands file that compares commands in the grammar toJim 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
2020-02-16Show apostrophes and backticks in HTML, too.Jim Fehrle
2020-02-13Spell out the entry suffix in the main indexJim Fehrle
2020-01-27checkdeps.py: report *all* missing dependencies at oncePaolo G. Giarrusso
2020-01-27checkdeps: check for sphinxcontrib-bibtexPaolo G. Giarrusso
2020-01-03[tools] Remove support for python2Emilio Jesus Gallego Arias
2019-12-28Prevent apostrophes and backticks from being stylized in latexJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 07:27:21 +0000