aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram
AgeCommit message (Expand)Author
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-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-08Convert Ltac chapter to prodnJim 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-05-15Document new Search features.Théo Zimmermann
2020-05-15Update docgram following #12122 and #12229.Théo Zimmermann
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:25:17 +0000