coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix some coq-tex errors in the reference manual.	Guillaume Melquiond	2017-07-28
\|
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
*	Indexing and documenting some options.	Pierre-Marie Pédrot	2015-12-12
\|
*	Separate index for vernacular options.	Maxime Dénès	2015-02-17
\|
*	Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).	Hugo Herbelin	2014-10-03
\|
*	Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵	Arnaud Spiwack	2014-09-04
\| \| \| \|	Schemes] option.
*	Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"	Hugo Herbelin	2014-07-01
\|
*	Port rewrites of tactic documentation from branch 8.4.	gmelquio	2012-09-15
	This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277, r15278, r15337. The merge did not go without troubles, but hopefully none of the changes were lost in process. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7