aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Collapse)Author
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-09-18Fix Removed in Sphinx 4 deprecations.Théo Zimmermann
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11Turn integer into natural in several mlgsPierre Roux
Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
2020-09-11[refman] Explicit integer and naturalPierre Roux
As respectively bigint and bignat that fit into an OCaml int.
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename numeral to numberPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-11[parsing] Simplify bigintPierre Roux
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-09-11Remove outdated references to productionlist.Théo Zimmermann
2020-09-09Merge PR #12994: Fix docgram's dune file following #12085.coqbot-app[bot]
Reviewed-by: ejgallego
2020-09-08Fix docgram's dune file following #12085.Théo Zimmermann
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-07-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
filtered-only show Ltac2 tags outside of ltac2.rst
2020-07-08Make local nonterminal definitions unique when necessaryJim Fehrle
2020-06-09Merge PR #12103: Convert Ltac chapter to prodnThéo Zimmermann
2020-06-08Convert Ltac chapter to prodnJim Fehrle
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-08Add NOTINRSTS nonterminal to suppress messagesJim Fehrle
2020-06-08Report an error for empty (sub)productionsJim Fehrle
(Sphinx notations don't support these.)
2020-06-08Add MOVEALLBUT operationJim Fehrle
2020-06-08Refactor SELF code for clarityJim Fehrle
Handle SELF within nested constructs more clearly
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 14:05:58 +0000