coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.	Pierre-Marie Pédrot	2016-03-06
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\
\| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
\| *	Fix a typo in dev/doc/changes.txt	Jason Gross	2016-03-04
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Compile OS X binaries without native_compute support.	Maxime Dénès	2016-01-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fixing #4467 (continued).	Hugo Herbelin	2016-01-13
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fix order of files in mllib.	Maxime Dénès	2016-01-05
* \| \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
* \| \|	Finer-grained types for toplevel values.	Pierre-Marie Pédrot	2015-12-21
* \| \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
\| \|/ \|/\|
* \|	Tying the loop in tactic printing API.	Pierre-Marie Pédrot	2015-12-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Fixing a minor problem in Makefile.build that was prevening "dev/printers.cma...	Matej Kosik	2015-12-07
\| *	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Factorizing unsafe code by relying on the new Dyn module.	Pierre-Marie Pédrot	2015-12-05
* \|	Ensuring that documentation of mli code works in the presence of utf-8	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Update history of revisions.	Hugo Herbelin	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	MacOS package script: do not fail if link to /Applications already exists.	Maxime Dénès	2015-11-18
\| *	Being more precise and faithful about the origin of the file reporting	Hugo Herbelin	2015-11-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	MacOS package script: do not fail if directory _dmg already exists.	Maxime Dénès	2015-11-13
\| *	Script building MacOS package.	Maxime Dénès	2015-11-12
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\|
\| *	Fixing another instance of bug #3267 in eauto, this time in the	Hugo Herbelin	2015-10-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Refine Gregory Malecha's patch on VM and universe polymorphism.	Maxime Dénès	2015-10-28
\| *	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
* \|	Type-safe Egramml.grammar_prod_item.	Pierre-Marie Pédrot	2015-10-27
* \|	Pcoq entries are given a proper module.	Pierre-Marie Pédrot	2015-10-26
* \|	Adding a notion of monotonous evarmap.	Pierre-Marie Pédrot	2015-10-18
* \|	Dedicated file for universe unification context manipulation.	Pierre-Marie Pédrot	2015-10-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Reverting modifications in dev/top_printers pushed mistakenly.	Pierre-Marie Pédrot	2015-10-14
\| *	Fixing perfomance issue of auto hints induced by universes.	Pierre-Marie Pédrot	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	Code cleaning in VM (with Benjamin).	Maxime Dénès	2015-10-09
\| *	Minor typo in universe polymorphism doc.	Maxime Dénès	2015-10-09
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06