aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_interp.c
Commit message (Expand)AuthorAge
* Make some comments more precise about compilation of cofixpointsGravatar Maxime Dénès2018-05-28
* Wrap VM bytecode used on the OCaml side in an OCaml block.Gravatar Pierre-Marie Pédrot2018-04-30
* Moving the VM global atom table to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
* Moving the VM global data to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
* Handle application of a primitive projection to a not yet evaluated cofixpoin...Gravatar Guillaume Melquiond2016-12-23
* Fix #5248 - test-suite fails in 8.6beta1Gravatar Maxime Dénès2016-12-06
* Fix incorrect long multiplication in the VM.Gravatar Guillaume Melquiond2016-11-24
* 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
* | More comments in VM.Gravatar Maxime Dénès2016-10-19
* | 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
* 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
* 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
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
* 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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 22:54:46 +0000