aboutsummaryrefslogtreecommitdiff
path: root/kernel/vconv.ml
AgeCommit message (Expand)Author
2016-10-19More comments in VM.Maxime Dénès
2016-08-10Make code a bit clearer by removing optional argument.Guillaume Melquiond
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2015-10-28Refine Gregory Malecha's patch on VM and universe polymorphism.Maxime Dénès
2015-10-28Conversion of polymorphic inductive types was incomplete in VM and native.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-14Remove -vm flag of coqtop.Maxime Dénès
2015-10-14Remove unused infos structure in VM.Maxime Dénès
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-03-27use a more compact representation of non-constant constructorsBenjamin Gregoire
2015-03-26Fix bug 4157,Benjamin Gregoire
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-04Fixing pervasives equalities in Vconv.Pierre-Marie Pédrot
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-03-08adding eta in the vmbgregoir
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2006-10-05Correction de deux cas où les types inductifs n'étaient pas comparésherbelin
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2005-12-05correction bug 881.gregoire
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-02Types inductifs parametriquesmohring
2005-02-12Uniformisation de destApplication en destAppherbelin
2004-11-22Code mortherbelin
2004-11-22compatibility with POWERPCgregoire
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:56:26 +0000