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
*
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