coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵	Zeimer	2018-07-19
\| \| \| \|	of the Reference Manual.
*	Fixed some typos and grammar errors from section 'The language' of the ↵	Zeimer	2018-07-19
\| \| \| \|	Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes.
*	Remove fourier plugin	Maxime Dénès	2018-07-17
\| \| \| \|	As stated in the manual, the fourier tactic is subsumed by lra.
*	Improve the section Terms of the Gallina chapter.	Théo Zimmermann	2018-05-26
\| \| \| \|	Including adding missing irrefutable-patterns to the grammar of binders.
*	[Sphinx] Fix all remaining warnings.	Maxime Dénès	2018-04-14
\|
*	[sphinx] Fix many warnings.	Théo Zimmermann	2018-04-14
\| \| \| \| \|	Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
*	[sphinx] Remove migration artefacts.	Théo Zimmermann	2018-04-11
\| \| \| \| \|	These were used very inconsistenty, serve no purpose and the link to the source is particularly useless because it's a moving target.
*	[Sphinx] Add chapter 3	Maxime Dénès	2018-03-15
\| \| \| \|	Thanks to Pierre Letouzey for porting this chapter.
*	[Sphinx] Move chapter 3 to new infrastructure	Maxime Dénès	2018-03-15