aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Expand)Author
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] Document the via ... using ... optionPierre Roux
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-10-30Renaming numnotoption into number_modifierPierre Roux
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename tac2type -> ltac2_type,Jim Fehrle
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-22Make no match/multiple match for tacn/cmd an errorJim Fehrle
2020-10-20Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loopcoqbot-app[bot]
2020-10-19Better message and avoid an infinite SPLICE loopJim Fehrle
2020-10-12Add missing ";" in record grammarJim Fehrle
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]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
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
2020-09-11[refman] Explicit integer and naturalPierre Roux
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]
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
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
2020-06-08Add NOTINRSTS nonterminal to suppress messagesJim Fehrle
2020-06-08Report an error for empty (sub)productionsJim Fehrle
2020-06-08Add MOVEALLBUT operationJim Fehrle
2020-06-08Refactor SELF code for clarityJim Fehrle
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:: di...Clément Pit-Claudel
2020-06-06Match only a single line as the coqtop promptJim Fehrle
2020-06-05Fix comment.Théo Zimmermann
2020-06-05[sphinx] Fix #12361Clément Pit-Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:57:35 +0000