index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
vm.mli
Age
Commit message (
Expand
)
Author
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-01-26
Safer VM interfaces
Maxime Dénès
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2015-12-09
bug fixes to vm computation + test cases.
Gregory Malecha
2015-10-28
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-09
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-07-05
Fix handling of primitive projections in VM.
Maxime Dénès
2015-03-27
use a more compact representation of non-constant constructors
Benjamin Gregoire
2015-03-26
Fix bug 4157,
Benjamin Gregoire
2015-01-15
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2012-12-14
Modulification of identifier
ppedrot
2012-10-02
Remove some dead code in the vm
letouzey
2011-03-08
adding eta in the vm
bgregoir
2010-04-29
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2009-11-13
Move Obj.magic call to the Vm module
glondu
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2006-07-22
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2004-11-22
compatibility with POWERPC
gregoire
2004-11-12
Changement dans les boxed values .
gregoire
2004-10-20
COMMITED BYTECODE COMPILER
barras