aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\
| * Fix potential race condition in vm_compute.Gravatar Guillaume Melquiond2016-05-31
* | Remove int64 emulation in bytecode interpreter.Gravatar Maxime Dénès2016-03-25
|/
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Make interpreter of PROJ simpler by not using the stack.Gravatar Guillaume Melquiond2015-10-14
* Remove some unused variables.Gravatar Guillaume Melquiond2015-10-14
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Gravatar Maxime Dénès2015-09-06
* Fixed critical bug in 31 bit arithmetic of VMGravatar Catalin Hritcu2015-09-06
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* Making Coq compile with ocp-memprof.Gravatar Pierre-Marie Pédrot2015-06-01
* Fix some ill-typed debugging code in the VM.Gravatar Guillaume Melquiond2015-04-27
* 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
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Remove some dead code in the vmGravatar letouzey2012-10-02
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Fix thumb2-related build errorGravatar glondu2011-04-19
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
* Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)Gravatar letouzey2011-04-01
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* ocamlbuild improvements + minor makefile fixGravatar letouzey2009-03-24
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Rely on ocamlc to call the C compiler...Gravatar glondu2008-09-04
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* patch for C code of addmuldiv31Gravatar thery2008-02-27
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
* corrections bug dans l'implem de int31Gravatar bgregoir2007-05-15
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
* Appel à caml_modify pour Ocaml 3.07Gravatar notin2006-09-01
* Modifications dans les scripts de configuration (coqtop et coqide affichent m...Gravatar notin2006-07-28
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Changement des named_contextGravatar gregoire2005-12-02
* compatibility with POWERPCGravatar gregoire2004-11-22
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20