index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
byterun
/
coq_fix_code.c
Commit message (
Expand
)
Author
Age
*
Wrap VM bytecode used on the OCaml side in an OCaml block.
Pierre-Marie Pédrot
2018-04-30
*
Fix #5127 Memory corruption with the VM
Maxime Dénès
2016-10-24
*
Fix handling of primitive projections in VM.
Maxime Dénès
2015-07-05
*
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
*
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
*
Rely on ocamlc to call the C compiler...
glondu
2008-09-04
*
ajout de head0 et tail0 en natif
bgregoir
2007-06-20
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Changement dans le kernel :
bgregoir
2006-12-11
*
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2006-07-22
*
compatibility with POWERPC
gregoire
2004-11-22
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20