index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
cemitcodes.mli
Commit message (
Expand
)
Author
Age
*
Use a more compact representation for bytecode relocations stored on disk.
Pierre-Marie Pédrot
2018-02-14
*
Move the call to the computation of bytecode inside Cemitcodes.
Pierre-Marie Pédrot
2018-02-14
*
Abstract further the type of VM bytecode compilation.
Pierre-Marie Pédrot
2018-02-14
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
|
Exporting a purely functional interface to bytecode patching.
Pierre-Marie Pédrot
2015-10-16
|
/
*
Fixing some English misspelling.
Hugo Herbelin
2015-07-29
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
fixed bug 2580. Quick fix: copy emitcodes before patching it
barras
2011-08-01
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
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
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20