coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\
\| *	STM: Print/Extraction have to be skipped if -quick	Enrico Tassi	2016-02-19
\| *	STM: classify some variants of Instance as regular `Fork nodes.	Enrico Tassi	2016-02-19
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	STM: always stock in vio files the first node (state) of a proof	Enrico Tassi	2016-02-10
\| * \|	STM: not delegate proofs that contain Vernac(Module\|Require\|Import), #4530	Enrico Tassi	2016-02-10
\| \| *	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ \|/\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \|	CLEANUP: removing unnecessary wrapper	Matej Kosik	2016-01-11
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-05
\|\\|
\| *	fixup d2b468a, evar normalization is needed	Enrico Tassi	2016-01-04
\| *	par: check if the goal is not ground and fail (fix #4465)	Enrico Tassi	2016-01-04
\| *	workers: purge short version of -load-vernac too (fix #4458)	Enrico Tassi	2016-01-04
* \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \|	Remove some useless module opening.	Guillaume Melquiond	2016-01-02
* \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \|	Remove unused functions.	Guillaume Melquiond	2016-01-01
* \|	Remove useless recursive flags.	Guillaume Melquiond	2016-01-01
* \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
* \|	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
* \|	CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...	Matej Kosik	2015-12-18
* \|	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
* \|	Specializing the Dyn module to each usecase.	Pierre-Marie Pédrot	2015-12-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	vio: fix argument parsing (progress on #4442)	Enrico Tassi	2015-12-01
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: correctly register universe binders for lemmas.	Matthieu Sozeau	2015-11-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico.	Maxime Dénès	2015-11-02
\| *	STM: fix undo into a branch containing side effects	Enrico Tassi	2015-11-02
\| *	STM: never reopen a branch containing side effects	Enrico Tassi	2015-11-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\|
\| *	Add a way to get the right fix_exn in external vernacular commands	Matthieu Sozeau	2015-10-30
\| *	Handle side-effects of Vernacular commands inside proofs better, so that	Matthieu Sozeau	2015-10-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Miscellaneous typos, spacing, US spelling in comments or variable names.	Hugo Herbelin	2015-10-18
* \|	Clarifying and documenting the UState API.	Pierre-Marie Pédrot	2015-10-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	When typechecking a lemma statement, try to resolve typeclasses before	Matthieu Sozeau	2015-10-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	STM: Work around an occasional crash in dot (debug output)	Alec Faithfull	2015-10-09
\| *	TQueue: Allow some tasks to be saved when clearing a TQueue	Alec Faithfull	2015-10-09
\| *	TQueue: Expose the length of TQueues	Alec Faithfull	2015-10-09
\| *	STM: Added functions for saving and restoring the internal state	Alec Faithfull	2015-10-09