aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram
AgeCommit message (Collapse)Author
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
(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-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
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-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
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-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-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-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-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.
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
for integers and natural nums
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
and inserting it into the .rst files
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 18:51:46 +0000