coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-06-14	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey
	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.
2017-03-23	Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."	Maxime Dénès
	This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
2017-03-23	Add empty Extraction.v and FunInd.v to prepare landing of PR#220.	Maxime Dénès
	This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.