coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Refolding: disable in 8.4 compat file, document	Matthieu Sozeau	2016-09-12
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\|\
\| *	Fix bug #5043: [Admitted] lemmas pick up section variables.	Pierre-Marie Pédrot	2016-08-31
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\\|
\| *	Compat84: Don't mess with stdlib modules	Jason Gross	2016-07-05
\| *	Unbreak singleton list-like notation (-compat 8.4)	Jason Gross	2016-06-09
* \|	Relying instead on the Coq85 inclusion!	Hugo Herbelin	2016-06-06
* \|	Mode "Bracketing Last Introduction Pattern" is on for 8.4	Hugo Herbelin	2016-06-06
* \|	Mode "Regular Subst Tactic" is on in 8.6.	Hugo Herbelin	2016-06-06
* \|	Merge remote-tracking branch 'github/pr/118' into trunk	Maxime Dénès	2016-06-06
\|\ \ \| \|/ \|/\|
* \|	Removing unexcepted activation of option "Regular Subst Tactic", since	Hugo Herbelin	2016-05-14
* \|	Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...	Pierre Letouzey	2016-05-04
\|\ \
* \| \|	Added compatibility coercions from Specif.v which were present in Coq 8.4.	Hugo Herbelin	2016-04-08
* \| \|	Add -compat 8.4 econstructor tactics, and tests	Jason Gross	2016-04-05
* \| \|	Fix bug #4656	Jason Gross	2016-04-05
* \| \|	Update Coq84.v	Jason Gross	2016-04-04
* \| \|	Add compatibility Nonrecursive Elimination Schemes	Jason Gross	2016-04-04
* \| \|	Update copyright headers.	Maxime Dénès	2016-01-20
\| \| *	Update Coq84.v	Jason Gross	2016-01-12
\| \|/ \|/\|
\| *	Move compatibility notations to their proper files	Jason Gross	2015-12-29
\|/
*	Moved proof_admitted to its own file, named "AdmitAxiom.v".	Maxime Dénès	2015-12-14
*	Update compatibility file for some of bug #4392	Jason Gross	2015-11-03
*	Add compatibility files (feature 4319)	Jason Gross	2015-09-30