coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot	2015-01-23
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-01-23
\|\
\| *	Extraction: fix #3629.	Maxime Dénès	2015-01-23
\| *	Add the possibility of defining opaque terms with program.	mlasson	2015-01-21
\| *	Reference Manual/Credits: expand the paragraph on the new proof engine to mat...	Arnaud Spiwack	2015-01-21
\| *	Reference Manual/Credits: native compute is a major contribution.	Arnaud Spiwack	2015-01-21
\| *	Reference manual/Credits: populate the "various smaller-scale improvements" p...	Arnaud Spiwack	2015-01-21
\| *	Reference Manual/Credits: remove a duplicate.	Arnaud Spiwack	2015-01-21
\| *	Reference manual: pass over the credit section for English.	Arnaud Spiwack	2015-01-21
\| *	Reference manual: fix typo in doc of [tryif/then/else].	Arnaud Spiwack	2015-01-21
* \|	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot	2015-01-21
\| *	Fix a critical bug in machine arithmetic for native compiler.	Maxime Dénès	2015-01-20
* \|	Making unification of LetIn's expressions more consistent (see #3920).	Hugo Herbelin	2015-01-19
\| *	Making unification of LetIn's expressions more consistent (see #3920).	Hugo Herbelin	2015-01-19
\| *	Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was	Maxime Dénès	2015-01-18
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-01-17
\|\\|
\| *	Remove dead code.	Maxime Dénès	2015-01-17
\| *	Fix #3379, now that Require inside modules is allowed again.	Maxime Dénès	2015-01-17
* \|	Merge branch '8.5' into trunk	Matthieu Sozeau	2015-01-18
\|\\|
* \|	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-18
* \|	Univs: Complete documentation in refman.	Matthieu Sozeau	2015-01-18
* \|	Partially revert "Forbid Require inside interactive modules and module types."	Maxime Dénès	2015-01-18
* \|	Revert "Adapting two files from test-suite to now forbidden Require's in modu...	Maxime Dénès	2015-01-18
* \|	Revert "Update test for #3363 now that Require is forbidden inside modules."	Maxime Dénès	2015-01-18
* \|	Revert "Fix files in test-suite having to do with Require inside modules."	Maxime Dénès	2015-01-18
* \|	Avoid compilation warning... might not be the best fix though.	Matthieu Sozeau	2015-01-18
* \|	Univs: Fix alias computation for VMs, computation of normal form of	Matthieu Sozeau	2015-01-18
* \|	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-18
* \|	coq_makefile: install also .v and .glob	Enrico Tassi	2015-01-18
* \|	Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"	Matthieu Sozeau	2015-01-18
* \|	vm_printers: fix compilation	Enrico Tassi	2015-01-18
* \|	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-18
* \|	Minor fixes to the refman credits to be continued.	Matthieu Sozeau	2015-01-18
* \|	Move explanations about primitive projections to the manual.	Matthieu Sozeau	2015-01-18
* \|	Add a (by default deactivated) option to force typeclass resolution to	Matthieu Sozeau	2015-01-18
* \|	Expand Credits for 8.5 and doc on universes	Matthieu Sozeau	2015-01-18
* \|	Remove typeclass opaque directive, some proofs in the stdlib rely on it being...	Matthieu Sozeau	2015-01-18
* \|	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau	2015-01-18
* \|	Update header of CHANGES.	Maxime Dénès	2015-01-18
\| *	There was one more universe needed due to the use of now non-universe-polymor...	Matthieu Sozeau	2015-01-18
\| *	Back to 4 expected universes.	Matthieu Sozeau	2015-01-17
\| *	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
\| *	Univs: Complete documentation in refman.	Matthieu Sozeau	2015-01-17
\| *	Partially revert "Forbid Require inside interactive modules and module types."	Maxime Dénès	2015-01-17
\| *	Revert "Adapting two files from test-suite to now forbidden Require's in modu...	Maxime Dénès	2015-01-17
\| *	Revert "Update test for #3363 now that Require is forbidden inside modules."	Maxime Dénès	2015-01-17
\| *	Revert "Fix files in test-suite having to do with Require inside modules."	Maxime Dénès	2015-01-17
\| *	Avoid compilation warning... might not be the best fix though.	Matthieu Sozeau	2015-01-17
\| *	Univs: Fix alias computation for VMs, computation of normal form of	Matthieu Sozeau	2015-01-17
\| *	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17