coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)	Pierre Letouzey	2017-10-07
*	Adding a V8.7 compatibility version number.	Hugo Herbelin	2017-07-21
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Put plugin exports in the right compatibility file	Jason Gross	2017-06-22
*	Merge PR#375: Deprecation	Maxime Dénès	2017-06-15
\|\
* \|	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
\| *	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
\|/
*	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik	2017-06-01
*	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\|\
\| *	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
* \|	Silence option deprecation warnings in the compat file	Jason Gross	2016-11-04
\| *	Add Unset Use Unif Heuristics in Compat/Coq85	Matthieu Sozeau	2016-10-22
\|/
*	Fix previous commit.	Pierre-Marie Pédrot	2016-10-17
*	Merge PR #300 into v8.6	Pierre-Marie Pédrot	2016-10-17
\|\
* \|	Clean up type classes flags and update compat file.	Maxime Dénès	2016-10-05
\| *	Move vector/list compat notations to their relevant files	Jason Gross	2016-09-29
\|/
*	Remove spaces from around list notations	Jason Gross	2016-09-26
*	Unbreak Ltac [ \| .. \| ] notation in -compat 8.5	Jason Gross	2016-09-26
*	Fix bug #4785 (use [ ] for vector nil)	Jason Gross	2016-09-26
*	Refolding: disable in 8.4 compat file, document	Matthieu Sozeau	2016-09-12
*	no-refold patch	Paul Steckler	2016-09-09
*	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
\|\\|
* \|	Fix #4793: Coq 8.6 should accept -compat 8.6	Maxime Dénès	2016-07-06
\| *	Compat84: Don't mess with stdlib modules	Jason Gross	2016-07-05
* \|	Add Unset Shrink Abstract/Obligations in Coq85	Matthieu Sozeau	2016-06-27
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
\| *	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
\|\ \
* \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-20
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Removing unexcepted activation of option "Regular Subst Tactic", since	Hugo Herbelin	2016-05-14
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\| \|
\| * \|	Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...	Pierre Letouzey	2016-05-04
\| \|\ \
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\\| \| \|
\| * \| \|	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
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \| \|
\| * \| \|	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
\| \|/
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\|
\| *	Moved proof_admitted to its own file, named "AdmitAxiom.v".	Maxime Dénès	2015-12-14
* \|	Updating Compat85.v after bd1c97653 on bracketing last or-and	Hugo Herbelin	2015-11-10
\|/