aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vconv.ml
Commit message (Expand)AuthorAge
* 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