coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Unify pre_env and env	Maxime Dénès	2018-05-28
*	Remove vm_conv hook and reorganize kernel files	Maxime Dénès	2018-05-28
*	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\
\| *	Handling evars in the VM.	Pierre-Marie Pédrot	2018-03-03
* \|	[VM] Unify Const_sorts and Const_type, and remove Vsort.	Maxime Dénès	2018-03-02
\|/
*	Safer VM interfaces	Maxime Dénès	2018-01-26
*	[kernel] Patch allowing to disable VM reduction.	Emilio Jesus Gallego Arias	2017-12-02
*	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	More comments in VM.	Maxime Dénès	2016-10-19
*	Make code a bit clearer by removing optional argument.	Guillaume Melquiond	2016-08-10
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Refine Gregory Malecha's patch on VM and universe polymorphism.	Maxime Dénès	2015-10-28
*	Conversion of polymorphic inductive types was incomplete in VM and native.	Maxime Dénès	2015-10-28
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
*	Remove -vm flag of coqtop.	Maxime Dénès	2015-10-14
*	Remove unused infos structure in VM.	Maxime Dénès	2015-10-14
*	Code cleaning in VM (with Benjamin).	Maxime Dénès	2015-10-09
*	Fix handling of primitive projections in VM.	Maxime Dénès	2015-07-05
*	use a more compact representation of non-constant constructors	Benjamin Gregoire	2015-03-27
*	Fix bug 4157,	Benjamin Gregoire	2015-03-26
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Make kernel reduction code parametric over the handling of universes,	Matthieu Sozeau	2014-06-06
*	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing pervasives equalities in Vconv.	Pierre-Marie Pédrot	2014-03-04
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	adding eta in the vm	bgregoir	2011-03-08
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	correction bug 881.	gregoire	2005-12-05
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Types inductifs parametriques	mohring	2005-11-02
*	Uniformisation de destApplication en destApp	herbelin	2005-02-12
*	Code mort	herbelin	2004-11-22
*	compatibility with POWERPC	gregoire	2004-11-22