aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.ml
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \
| * | Handling evars in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
* | | [VM] Unify Const_sorts and Const_type, and remove Vsort.Gravatar Maxime Dénès2018-03-02
|/ /
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
* Factorize the relocations in the on-disk VM representation.Gravatar Pierre-Marie Pédrot2018-02-14
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#189: Remove tabulation support from pretty-printing.Gravatar Maxime Dénès2017-02-20
|\
* \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
|\ \
| * | Fix #5127 Memory corruption with the VMGravatar Maxime Dénès2016-10-24
* | | Use a better data structure for VM compilation of free vars.Gravatar Pierre-Marie Pédrot2016-08-22
| | * Remove tabulation support from pretty-printing.Gravatar Guillaume Melquiond2016-06-02
| |/ |/|
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Refine Gregory Malecha's patch on VM and universe polymorphism.Gravatar Maxime Dénès2015-10-28
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Gather VM tags in Cbytecodes.Gravatar Maxime Dénès2015-10-12
* print universes when dumping bytecode.Gravatar Gregory Malecha2015-09-03
* a small amount of documentation on the virtual machine.Gravatar Gregory Malecha2015-07-23
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
* Fix bug 4157,Gravatar Benjamin Gregoire2015-03-26
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Modulification of identifierGravatar ppedrot2012-12-14
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)Gravatar herbelin2010-05-09
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 03:57:40 +0000