coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'yet-another-makefile-bigbang' into trunk	Pierre Letouzey	2016-06-01
\|\
\| *	Makefile: restore the use of coqdep_boot for creating .v.d files	Pierre Letouzey	2016-06-01
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\|/
*	Checker: avoid using obsolete names from Names	Pierre Letouzey	2016-05-31
*	Checker: no more -I kernel via a few symlinks (for Names and Esubst)	Pierre Letouzey	2016-05-31
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\
\| *	Make votour a bit more robust/forgiving with respect to user commands (bug #4...	Guillaume Melquiond	2016-05-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\\|
\| *	Fix missing newline in coqchk engagement (bug #4694).	Guillaume Melquiond	2016-04-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\\|
\| *	A patch renaming equal into eq in the module dealing with	Hugo Herbelin	2016-03-22
* \|	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
\| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \|	CLEANUP: Simplifying the changes done in "checker/*"	Matej Kosik	2016-02-15
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update cic.mli MD5 after header update.	Maxime Dénès	2016-01-20
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove deprecated command-line options such as "-as".	Guillaume Melquiond	2016-01-06
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\\|
\| *	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
\| *	Fix order of files in mllib.	Maxime Dénès	2016-01-05
* \|	Remove unused function Checker.print_loc.	Guillaume Melquiond	2015-12-31
* \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
* \|	Factorizing unsafe code by relying on the new Dyn module.	Pierre-Marie Pédrot	2015-12-05
* \|	Displaying the object identifier in votour.	Pierre-Marie Pédrot	2015-11-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Checker was forgetting to register global universes introduced by opaque	Matthieu Sozeau	2015-11-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	Univs: fix checker generating undeclared universes.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: update checker	Matthieu Sozeau	2015-10-02
\| \|/
\| *	Make the interface of System.raw_extern_intern much saner.	Guillaume Melquiond	2015-09-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\\|
\| *	Implementing Herbelin's fix for the "NonPar" bug	mlasson	2015-09-03
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Hconsing continued	Hugo Herbelin	2015-08-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\|
\| *	Univs/Inductive: fix typechecking of cases	Matthieu Sozeau	2015-07-15
\| *	Updating checksum in checker (9c732a5cc continued).	Hugo Herbelin	2015-07-12
\| *	Unused variables reported by OCaml.	Hugo Herbelin	2015-07-10
\| *	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
\| *	Kernel/Checker: Cleanup fixes of substitutions due to let-ins.	Matthieu Sozeau	2015-07-09
\| *	Template polymorphism: A bug-fix for Bug #4258	mlasson	2015-07-09
\| *	Checker: Report bugfixes from kernel/inductive.ml	Matthieu Sozeau	2015-07-08
\| *	Checker: Fix bug #4282	Matthieu Sozeau	2015-07-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\\|
\| *	Adding a more efficient representation of OCaml objects in votour.	Pierre-Marie Pédrot	2015-06-25
\| *	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-25