coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\\|
\| *	On-demand Require.	Pierre-Marie Pédrot	2015-06-24
\| *	Splitting the library representation on disk in two.	Pierre-Marie Pédrot	2015-06-24
* \|	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-23
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	Votour displays wordsize of segments before loading them.	Pierre-Marie Pédrot	2015-06-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Removing references to deprecated syntax -I/-R -as.	Pierre-Marie Pédrot	2015-03-31
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	Exporting memory representation of STM tasks for votour.	Pierre-Marie Pédrot	2015-03-25
\| *	Functorized interface over object representation in votour.	Pierre-Marie Pédrot	2015-03-24
\| *	Fixing representation of dynamics in votour (again).	Pierre-Marie Pédrot	2015-03-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	coqchk: more prints when -debug	Enrico Tassi	2015-03-23
\| *	Fixing internal representation of Dyn.t in votour.	Pierre-Marie Pédrot	2015-03-18
\| *	Now accepting unit props in mutual definitions	Bruno Barras	2015-03-02
* \|	Now accepting unit props in mutual definitions	Bruno Barras	2015-03-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\\|
\| *	Fix checker after addition of a universe context in with t := c constraints.	Matthieu Sozeau	2015-02-26
* \|	Using same code for browsing physical directories in coqtop and coqdep.	Hugo Herbelin	2015-02-16
\| *	Revert "Using same code for browsing physical directories in coqtop and coqdep."	Hugo Herbelin	2015-02-12
\| *	Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)	Hugo Herbelin	2015-02-12