aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vconv.ml
Commit message (Expand)AuthorAge
* When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* More comments in VM.Gravatar Maxime Dénès2016-10-19
* Make code a bit clearer by removing optional argument.Gravatar Guillaume Melquiond2016-08-10
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Refine Gregory Malecha's patch on VM and universe polymorphism.Gravatar Maxime Dénès2015-10-28
* Conversion of polymorphic inductive types was incomplete in VM and native.Gravatar Maxime Dénès2015-10-28
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Remove -vm flag of coqtop.Gravatar Maxime Dénès2015-10-14
* Remove unused infos structure in VM.Gravatar Maxime Dénès2015-10-14
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
* Fix bug 4157,Gravatar Benjamin Gregoire2015-03-26
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing pervasives equalities in Vconv.Gravatar Pierre-Marie Pédrot2014-03-04
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* adding eta in the vmGravatar bgregoir2011-03-08
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* correction bug 881.Gravatar gregoire2005-12-05
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Uniformisation de destApplication en destAppGravatar herbelin2005-02-12
* Code mortGravatar herbelin2004-11-22
* compatibility with POWERPCGravatar gregoire2004-11-22
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20