coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-01-30	[toplevel] Deprecate the `-compile` flag in favor of `coqc`.	Emilio Jesus Gallego Arias
	This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2018-09-20	Rewrite "Flags, Options and Tables" section.	Jim Fehrle
	Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag:
2018-09-20	[doc] Include the rst and LaTeX preambles automatically in all files	Clément Pit-Claudel

2018-08-01	Improved grammar and spelling in the remaining chapters of the Reference Manual.	Zeimer

2018-04-14	[sphinx] Fix many warnings.	Théo Zimmermann
	Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
2018-04-04	[Sphinx] Add chapter 28	Maxime Dénès
	Thanks to Paul Steckler for porting this chapter.
2018-04-04	[Sphinx] Move chapter 28 to new infrastructure	Maxime Dénès