index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
Age
Commit message (
Expand
)
Author
2018-05-28
Fix #7333: vm_compute segfaults / Anomaly with cofix
Maxime Dénès
2018-05-28
Unify pre_env and env
Maxime Dénès
2018-05-28
Remove vm_conv hook and reorganize kernel files
Maxime Dénès
2018-05-28
Make some comments more precise about compilation of cofixpoints
Maxime Dénès
2018-05-28
Less confusing debug printing of setfield bytecode instruction
Maxime Dénès
2018-05-25
Merge pull request #7569 from ppedrot/clean-newring
Assia Mahboubi
2018-05-23
Renaming miscellaneous internal smart functions.
Hugo Herbelin
2018-05-23
Moving Rtree.smart_map into Rtree.Smart.map.
Hugo Herbelin
2018-05-23
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-23
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.
Hugo Herbelin
2018-05-23
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-21
Simplify the newring hack.
Pierre-Marie Pédrot
2018-05-16
Merge PR #7079: Remove naked pointers from the VM
Maxime Dénès
2018-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-04-30
Adapt the VM GC hook to handle the no-naked-pointers option flag.
Pierre-Marie Pédrot
2018-04-30
Make the VM accumulator look like an OCaml block.
Pierre-Marie Pédrot
2018-04-30
Wrap VM bytecode used on the OCaml side in an OCaml block.
Pierre-Marie Pédrot
2018-04-30
Merge PR #6958: [lib] Move global options to their proper place.
Maxime Dénès
2018-04-28
Merge PR #6892: Cleanup implementation of normalize_context_set a bit
Pierre-Marie Pédrot
2018-04-26
Always print explanation for univ inconsistency, rm Flags.univ_print
Gaëtan Gilbert
2018-04-20
Merge PR #6908: Move VM global tables from C to ML
Maxime Dénès
2018-04-13
universe normalisation: put equivalence class partition in UGraph
Gaëtan Gilbert
2018-04-12
Merge PR #6972: [api] Deprecate a couple of aliases that we missed.
Maxime Dénès
2018-04-09
Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation
Pierre-Marie Pédrot
2018-04-06
Fix #6956: Uncaught exception in bytecode compilation
Maxime Dénès
2018-04-02
[lib] Move global options to their proper place.
Emilio Jesus Gallego Arias
2018-03-28
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-27
Expliciting and taking advantage of a representation invariant in Esubst.
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-09
Fix expected number of arguments for cumulative constructors.
Gaëtan Gilbert
2018-03-09
Merge PR #6775: Allow using cumulativity without forcing strict constraints.
Maxime Dénès
2018-03-09
Merge PR #6769: Split closure cache and remove whd_both
Maxime Dénès
2018-03-09
Cumulativity: improve treatment of irrelevant universes.
Gaëtan Gilbert
2018-03-09
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
Merge PR #6747: Relax conversion of constructors according to the pCuIC model
Maxime Dénès
2018-03-09
Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values
Maxime Dénès
2018-03-08
Fix SR breakage due to allowing fixpoints on non-rec values
Matthieu Sozeau
2018-03-08
Relax conversion of constructors according to the pCuIC model
Matthieu Sozeau
2018-03-05
Add empty description for @raise statements to satisfy ocamldoc
mrmr1993
2018-03-05
Replace invalid tag @raises in ocamldoc comments with @raise
mrmr1993
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-04
Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort
Maxime Dénès
2018-03-04
Remove whd_both from the kernel.
Pierre-Marie Pédrot
2018-03-04
Pass the constant cache as a separate argument in kernel reduction.
Pierre-Marie Pédrot
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
[next]