index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
vmvalues.ml
Age
Commit message (
Expand
)
Author
2018-09-24
[kernel] Compile with almost all warnings enabled.
Emilio Jesus Gallego Arias
2018-09-17
OCaml now exports the min and max non-constant tags, let's use it
Maxime Dénès
2018-09-17
Add assertion on tags in eq_structured_constants
Maxime Dénès
2018-09-17
[VM] Inject structured constants in values without reallocating them.
Maxime Dénès
2018-09-17
[VM] Move structured_constant to Vmvalues
Maxime Dénès
2018-07-24
Projections use index representation
Gaëtan Gilbert
2018-06-10
[VM] Remove projection names from structured constants.
Maxime Dénès
2018-04-30
Wrap VM bytecode used on the OCaml side in an OCaml block.
Pierre-Marie Pédrot
2018-03-26
More efficient reallocation of VM global tables.
Pierre-Marie Pédrot
2018-03-26
Moving the VM global atom table to a ML reference.
Pierre-Marie Pédrot
2018-03-26
Moving the VM global data to a ML reference.
Pierre-Marie Pédrot
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-04
Merge PR #935: Handling evars in the VM
Maxime Dénès
2018-03-03
Handling evars in the VM.
Pierre-Marie Pédrot
2018-03-02
[VM] Unify Const_sorts and Const_type, and remove Vsort.
Maxime Dénès
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-12
Fix #6677: Critical bug with VM and universes
Maxime Dénès
2018-01-26
Safer VM interfaces
Maxime Dénès