aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Expand)Author
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` into...Pierre-Marie Pédrot
2021-01-13Adjust the doc_grammar files.Théo Zimmermann
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
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
2020-12-09Allow any character in a tacn, cmd, ... nameJim Fehrle
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-23Add COPYALL and APPENDALL edit ops, drop unneeded codeJim Fehrle
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...coqbot-app[bot]
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18Run doc_grammar for #13312.Théo Zimmermann
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
2020-11-16Update grammar in docJim Fehrle
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
2020-11-15Merge PR #13368: Fix dune rules for @check-gram following recent changes.coqbot-app[bot]
2020-11-15Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve d...coqbot-app[bot]
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-13Fix dune rules for @check-gram following recent changes.Théo Zimmermann
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
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]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:15:14 +0000