aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cemitcodes.ml
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [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
|/
* Factorize the relocations in the on-disk VM representation.Gravatar Pierre-Marie Pédrot2018-02-14
* Use a more compact representation for bytecode relocations stored on disk.Gravatar Pierre-Marie Pédrot2018-02-14
* Do not use global variables for VM bytecode compilation in Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
* Remove the unsafe bytes conversion function in Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
* Move the call to the computation of bytecode inside Cemitcodes.Gravatar Pierre-Marie Pédrot2018-02-14
* Abstract further the type of VM bytecode compilation.Gravatar Pierre-Marie Pédrot2018-02-14
* [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 branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
|\
| * In the Kami project, that causes a stack overflow in one of the example filesGravatar Paul Steckler2017-03-20
* | [misc] Remove warnings about String.setGravatar Emilio Jesus Gallego Arias2017-03-20
* | [safe_string] kernel/cemitcodesGravatar Emilio Jesus Gallego Arias2017-03-14
|/
* 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Removing dead code.Gravatar Pierre-Marie Pédrot2015-12-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * 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
* | Hashcons bytecode generated by the VM.Gravatar Pierre-Marie Pédrot2015-10-16
* | Exporting a purely functional interface to bytecode patching.Gravatar Pierre-Marie Pédrot2015-10-16
|/
* Fixing some English misspelling.Gravatar Hugo Herbelin2015-07-29
* Fix incomplete pattern-matching.Gravatar Matthieu Sozeau2015-07-22
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* fix code and bound for SWITCH instruction.Gravatar Benjamin Gregoire2015-03-30
* allows the vm to deal with inductive type with 8388607 constant constructors ...Gravatar Benjamin Gregoire2015-03-26
* More clever representation of substituted Cemitcode.Gravatar Pierre-Marie Pédrot2015-03-25
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* fixed bug 2580. Quick fix: copy emitcodes before patching itGravatar barras2011-08-01
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* 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
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Correction partielle du bug #1388 (augmentation de la taille des code accepte...Gravatar jforest2007-04-05