index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
vm.mli
Commit message (
Expand
)
Author
Age
*
bug fixes to vm computation + test cases.
Gregory Malecha
2015-12-09
*
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
*
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
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Modulification of identifier
ppedrot
2012-12-14
*
Remove some dead code in the vm
letouzey
2012-10-02
*
adding eta in the vm
bgregoir
2011-03-08
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Move Obj.magic call to the Vm module
glondu
2009-11-13
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- 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