aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytegen.ml
AgeCommit message (Expand)Author
2019-05-23Fixing typos - Part 2JPR
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-17OCaml now exports the min and max non-constant tags, let's use itMaxime Dénès
2018-09-17[VM] Inject structured constants in values without reallocating them.Maxime Dénès
2018-09-17[VM] Move structured_constant to VmvaluesMaxime Dénès
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
2018-07-24VM: don't duplicate projection narg information in lproj/kprojGaëtan Gilbert
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-27Fix #7723: vm_compute segfaults with universe polymorphismMaxime Dénès
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-12[VM] Rename reloc -> cenvMaxime Dénès
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-28Make some comments more precise about compilation of cofixpointsMaxime Dénès
2018-04-30Merge PR #6958: [lib] Move global options to their proper place.Maxime Dénès
2018-04-06Fix #6956: Uncaught exception in bytecode compilationMaxime Dénès
2018-04-02[lib] Move global options to their proper place.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime 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-02-27Update headers following #6543.Théo Zimmermann
2018-02-23New IR in VM: Clambda.Maxime Dénès
2018-02-12Fix #6677: Critical bug with VM and universesMaxime Dénès
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-24Fix #5127 Memory corruption with the VMMaxime Dénès
2016-10-19More comments in VM.Maxime Dénès
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-22Use a better data structure for VM compilation of free vars.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-12-09bug fixes to vm computation + test cases.Gregory Malecha
2015-10-28Refine Gregory Malecha's patch on VM and universe polymorphism.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:18:59 +0000