aboutsummaryrefslogtreecommitdiff
path: root/kernel/vconv.ml
AgeCommit message (Expand)Author
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-02-05Merge PR #9438: Cleanup universe length for inductives in vconvPierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-01-30Cleanup universe length for inductives in vconvGaëtan Gilbert
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-07-24Projections use index representationGaëtan Gilbert
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-03Handling evars in the VM.Pierre-Marie Pédrot
2018-03-02[VM] Unify Const_sorts and Const_type, and remove Vsort.Maxime Dénès
2018-01-26Safer VM interfacesMaxime Dénès
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:43:21 +0000