aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun/coq_interp.c
AgeCommit message (Expand)Author
2018-03-26Moving the VM global atom table to a ML reference.Pierre-Marie Pédrot
2018-03-26Moving the VM global data to a ML reference.Pierre-Marie Pédrot
2016-12-23Handle application of a primitive projection to a not yet evaluated cofixpoin...Guillaume Melquiond
2016-12-06Fix #5248 - test-suite fails in 8.6beta1Maxime Dénès
2016-11-24Fix incorrect long multiplication in the VM.Guillaume Melquiond
2016-10-26Merge branch 'v8.5' into v8.6Pierre-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-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Fix potential race condition in vm_compute.Guillaume Melquiond
2016-03-25Remove int64 emulation in bytecode interpreter.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-14Make interpreter of PROJ simpler by not using the stack.Guillaume Melquiond
2015-10-14Remove some unused variables.Guillaume Melquiond
2015-10-14Fix some typos.Guillaume Melquiond
2015-09-06Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Maxime Dénès
2015-09-06Fixed critical bug in 31 bit arithmetic of VMCatalin Hritcu
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-04-27Fix some ill-typed debugging code in the VM.Guillaume Melquiond
2015-03-30fix code and bound for SWITCH instruction.Benjamin Gregoire
2015-03-26allows the vm to deal with inductive type with 8388607 constant constructors ...Benjamin Gregoire
2015-03-13Fix compilation with forthcoming Ocaml version 4.03.Arnaud Spiwack
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2012-10-02Remove some dead code in the vmletouzey
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
2011-04-19Fix thumb2-related build errorglondu
2011-04-01CHANGES: a word about recent changes in coqide, about Ctrl-C in vmletouzey
2011-04-01Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)letouzey
2010-05-19Discontinue support for ocaml 3.09.*letouzey
2008-09-04Rely on ocamlc to call the C compiler...glondu
2008-05-27Correction du problème de complexité de Print Assumptions :aspiwack
2008-02-27patch for C code of addmuldiv31thery
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
2007-06-20ajout de head0 et tail0 en natifbgregoir
2007-05-15corrections bug dans l'implem de int31bgregoir
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2006-12-11Changement dans le kernel : bgregoir
2006-10-27changement des _sym par _comm dans setoid_ringbgregoir
2006-09-01Appel à caml_modify pour Ocaml 3.07notin
2006-07-28Modifications dans les scripts de configuration (coqtop et coqide affichent m...notin
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
2005-12-02Changement des named_contextgregoire
2004-11-22compatibility with POWERPCgregoire
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:28:21 +0000