aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Collapse)Author
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-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
2020-05-15Document new Search features.Théo Zimmermann
2020-05-15Update docgram following #12122 and #12229.Théo Zimmermann
2020-05-11Checking validity of coqdoc file name.Hugo Herbelin
This fixes #12265 (javascript injection vulnerability in file name).
2020-05-09Add a `with_strategy` tacticJason Gross
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g., `Opaque foo` doesn't break some automation which tries to unfold `foo`. We have some timeouts in the strategy success file. We should not run into issues, because we are not really testing how long these take. We could just as well use `Timeout 60` or longer, we just want to make sure the file dies more quickly rather than taking over 10^100 steps. Note that this tactic does not play well with `abstract`; I have a potentially controversial change that fixes this issue. One of the lines in the doc comes from https://github.com/coq/coq/pull/12129#issuecomment-619771556 Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr> Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr> Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
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
index Ack-by: Zimmi48
2020-04-29Support in-line glossary entries and referencesJim Fehrle
with an index
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
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
Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10Suppress the space after "#" when printing productionsJim Fehrle
to reflect lexer requirement for no space
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
Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants.
2020-04-02Merge PR #11869: Add an index for attributes.Clément Pit-Claudel
Reviewed-by: cpitclaudel
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
Reviewed-by: Zimmi48
2020-03-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
Fix makefile glitches
2020-03-29Merge PR #11938: Support for updating orderedGrammar with Dune.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
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
Use `dune build @check-gram --auto-promote` to automatically update these two files. You will need to run it twice if the two files need to be updated (which is the case most often) as Dune will stop after the first diff failure. The rst files are also updated but left in the `_build/` directory as Dune wouldn't support targets outside the current directory. You can just `mv _build/default/doc/sphinx doc` to update them after running the @check-gram target.
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics
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-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: ppedrot
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
following changes to attribute parsing.
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
Add headers to a few files which were missing them.
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
Show effect of edits to edited nt in PRINT Add cmdv:: info to prodnCommands Supporting code globally replaces a given "substring" in productions with another. (Substring over doc_symbols, not over characters.)
2020-02-24Generate prodnCommands file that compares commands in the grammar toJim Fehrle
those in the rsts.
2020-02-24Allow multiple indexed names on a single .. cmd::, etc.Jim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:42:48 +0000