aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_fix_code.c
Commit message (Expand)AuthorAge
* Wrap VM bytecode used on the OCaml side in an OCaml block.Gravatar Pierre-Marie Pédrot2018-04-30
* Fix #5127 Memory corruption with the VMGravatar Maxime Dénès2016-10-24
* 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
* Fix compilation with forthcoming Ocaml version 4.03.Gravatar Arnaud Spiwack2015-03-13
* Remove some dead code in the vmGravatar letouzey2012-10-02
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Rely on ocamlc to call the C compiler...Gravatar glondu2008-09-04
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* compatibility with POWERPCGravatar gregoire2004-11-22
* 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-05-17 05:00:43 +0000