index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
byterun
Commit message (
Expand
)
Author
Age
*
Adapt the VM GC hook to handle the no-naked-pointers option flag.
Pierre-Marie Pédrot
2018-04-30
*
Make the VM accumulator look like an OCaml block.
Pierre-Marie Pédrot
2018-04-30
*
Wrap VM bytecode used on the OCaml side in an OCaml block.
Pierre-Marie Pédrot
2018-04-30
*
Moving the VM global atom table to a ML reference.
Pierre-Marie Pédrot
2018-03-26
*
Moving the VM global data to a ML reference.
Pierre-Marie Pédrot
2018-03-26
*
Handle application of a primitive projection to a not yet evaluated cofixpoin...
Guillaume Melquiond
2016-12-23
*
Fix #5248 - test-suite fails in 8.6beta1
Maxime Dénès
2016-12-06
*
Fix incorrect long multiplication in the VM.
Guillaume Melquiond
2016-11-24
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-26
|
\
|
*
Fix #5127 Memory corruption with the VM
Maxime Dénès
2016-10-24
*
|
More comments in VM.
Maxime Dénès
2016-10-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
|
|
*
Fix potential race condition in vm_compute.
Guillaume Melquiond
2016-05-31
*
|
Remove int64 emulation in bytecode interpreter.
Maxime Dénès
2016-03-25
|
/
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
Make interpreter of PROJ simpler by not using the stack.
Guillaume Melquiond
2015-10-14
*
Remove some unused variables.
Guillaume Melquiond
2015-10-14
*
Fix some typos.
Guillaume Melquiond
2015-10-14
*
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
*
Fix a bug in 31 bit arithmetic, leading to failing conversion tests.
Maxime Dénès
2015-09-06
*
Fixed critical bug in 31 bit arithmetic of VM
Catalin Hritcu
2015-09-06
*
Fix handling of primitive projections in VM.
Maxime Dénès
2015-07-05
*
Making Coq compile with ocp-memprof.
Pierre-Marie Pédrot
2015-06-01
*
Fix some ill-typed debugging code in the VM.
Guillaume Melquiond
2015-04-27
*
fix code and bound for SWITCH instruction.
Benjamin Gregoire
2015-03-30
*
allows the vm to deal with inductive type with 8388607 constant constructors ...
Benjamin Gregoire
2015-03-26
*
Fix compilation with forthcoming Ocaml version 4.03.
Arnaud Spiwack
2015-03-13
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
Remove some dead code in the vm
letouzey
2012-10-02
*
fast bitwise operations (lor,land,lxor) on int31 and BigN
letouzey
2012-08-11
*
Fix thumb2-related build error
glondu
2011-04-19
*
CHANGES: a word about recent changes in coqide, about Ctrl-C in vm
letouzey
2011-04-01
*
Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)
letouzey
2011-04-01
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Discontinue support for ocaml 3.09.*
letouzey
2010-05-19
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
ocamlbuild improvements + minor makefile fix
letouzey
2009-03-24
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Rely on ocamlc to call the C compiler...
glondu
2008-09-04
*
Correction du problème de complexité de Print Assumptions :
aspiwack
2008-05-27
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
patch for C code of addmuldiv31
thery
2008-02-27
*
* Adding compability with ocaml 3.10 + camlp5 (rework of
letouzey
2007-09-15
*
ajout de head0 et tail0 en natif
bgregoir
2007-06-20
*
corrections bug dans l'implem de int31
bgregoir
2007-05-15
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Changement dans le kernel :
bgregoir
2006-12-11
*
changement des _sym par _comm dans setoid_ring
bgregoir
2006-10-27
*
Appel à caml_modify pour Ocaml 3.07
notin
2006-09-01
*
Modifications dans les scripts de configuration (coqtop et coqide affichent m...
notin
2006-07-28
[next]