coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-08	Convert Ltac chapter to prodn	Jim Fehrle

2020-06-08	Add NOTINRSTS nonterminal to suppress messages	Jim Fehrle

2020-06-08	Report an error for empty (sub)productions	Jim Fehrle
	(Sphinx notations don't support these.)
2020-06-08	Add MOVEALLBUT operation	Jim Fehrle

2020-06-08	Refactor SELF code for clarity	Jim Fehrle
	Handle SELF within nested constructs more clearly
2020-05-01	Move essential vocabulary and syntax conventions to section on basics.	Théo Zimmermann

2020-04-26	Convert syntax extensions chapter to prodn	Jim Fehrle

2020-04-10	Convert vernac commands chapter to prodn, update syntax	Jim Fehrle

2020-04-10	Suppress the space after "#" when printing productions	Jim Fehrle
	to reflect lexer requirement for no space
2020-04-10	Ignore subscripts in notation for matching cmds and tacs	Jim Fehrle

2020-04-10	Fix prefix matching	Jim Fehrle

2020-03-29	Add -no-update command line option to doc_grammar for Dune	Jim Fehrle
	Fix makefile glitches
2020-03-25	Doc_grammar: Update cmd:: and tacn:: constructs in .rsts	Jim Fehrle
	Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-03-09	Remove some productionlists	Jim Fehrle

2020-02-28	Convert Gallina Vernac to use prodn	Jim Fehrle

2020-02-24	Add OPTREF and INSERTALL editing operations	Jim 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-24	Generate prodnCommands file that compares commands in the grammar to	Jim Fehrle
	those in the rsts.
2019-12-28	Convert productionlists to prodns	Jim Fehrle

2019-11-20	Update grammar in the Terms section of Gallina chapter	Jim 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-28	Update documentation on tokens, use "int" and "num"	Jim Fehrle
	for integers and natural nums
2019-07-19	Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg files	Jim Fehrle
	and inserting it into the .rst files