coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-30	[dune] [docgram] Remove bash hack thanks to new option -no-update.	Théo Zimmermann

2020-03-30	Merge PR #11958: Add -no-update command line option to doc_grammar for Dune	Théo Zimmermann
	Reviewed-by: Zimmi48
2020-03-29	Add -no-update command line option to doc_grammar for Dune	Jim Fehrle
	Fix makefile glitches
2020-03-29	Merge PR #11938: Support for updating orderedGrammar with Dune.	Emilio Jesus Gallego Arias
	Reviewed-by: ejgallego
2020-03-28	Remove SearchAbout command, deprecated in 8.5	Jim Fehrle

2020-03-28	Update fullGrammar and orderedGrammar following #11877.	Théo Zimmermann

2020-03-28	New 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-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-25	Convert Gallina Extensions to use prodn	Jim Fehrle

2020-03-19	Update fullGrammar, common.edit_mlg and orderedGrammar...	Théo Zimmermann
	following changes to attribute parsing.
2020-03-19	Update fullGrammar and common.edit_mlg following #11839.	Théo Zimmermann

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-12	Dune build rules for doc_grammar and fullGrammar.	Théo Zimmermann

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