index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
vm.ml
Commit message (
Expand
)
Author
Age
*
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
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
|
/
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Refine Gregory Malecha's patch on VM and universe polymorphism.
Maxime Dénès
2015-10-28
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
Gather VM tags in Cbytecodes.
Maxime Dénès
2015-10-12
*
Complete handling of primitive projections in VM.
Maxime Dénès
2015-10-09
*
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
*
Fix handling of primitive projections in VM.
Maxime Dénès
2015-07-05
*
use a more compact representation of non-constant constructors
Benjamin Gregoire
2015-03-27
*
Fix bug 4157,
Benjamin Gregoire
2015-03-26
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Fixing generic hashes and replacing them with proper ones.
Pierre-Marie Pédrot
2014-03-03
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Remove some dead code in the vm
letouzey
2012-10-02
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Noise for nothing
pboutill
2012-03-02
*
adding eta in the vm
bgregoir
2011-03-08
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
better fix to bug #2319: types are compiled in the env of the bodies
barras
2010-07-30
*
fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodies
barras
2010-07-28
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
removed a potentially dangerous try ... with _ -> ...
barras
2010-07-16
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move Obj.magic call to the Vm module
glondu
2009-11-13
*
Removal of trailing spaces.
serpyc
2009-10-04
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
Protection contre les warnings 'unused variable' de ocaml 3.09
herbelin
2007-01-19
*
Changement dans le kernel :
bgregoir
2006-12-11
*
correction bug vm_compute
bgregoir
2006-08-25
*
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2006-07-22
*
changement d'egalite pour le named_context_val
gregoire
2005-12-05
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
compatibility with POWERPC
gregoire
2004-11-22
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20