aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Maxime Dénès2018-06-04
|\
* \ Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \
| * | Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* | | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* | | [api] Remove deprecated aliases from `Names`.Gravatar Emilio Jesus Gallego Arias2018-05-30
* | | [api] Reintroduce `Names.global_reference` aliasGravatar Emilio Jesus Gallego Arias2018-05-30
|/ /
* | Fix #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-28
* | Unify pre_env and envGravatar Maxime Dénès2018-05-28
* | Remove vm_conv hook and reorganize kernel filesGravatar Maxime Dénès2018-05-28
* | Make some comments more precise about compilation of cofixpointsGravatar Maxime Dénès2018-05-28
* | Less confusing debug printing of setfield bytecode instructionGravatar Maxime Dénès2018-05-28
* | Merge pull request #7569 from ppedrot/clean-newringGravatar Assia Mahboubi2018-05-25
|\ \
* | | Renaming miscellaneous internal smart functions.Gravatar Hugo Herbelin2018-05-23
* | | Moving Rtree.smart_map into Rtree.Smart.map.Gravatar Hugo Herbelin2018-05-23
* | | Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
* | | Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* | | Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Gravatar Hugo Herbelin2018-05-23
* | | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| * | Simplify the newring hack.Gravatar Pierre-Marie Pédrot2018-05-21
|/ /
* | Merge PR #7079: Remove naked pointers from the VMGravatar Maxime Dénès2018-05-16
|\ \
| | * Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Gaëtan Gilbert2018-05-13
| |/ |/|
* | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| * Adapt the VM GC hook to handle the no-naked-pointers option flag.Gravatar Pierre-Marie Pédrot2018-04-30
| * Make the VM accumulator look like an OCaml block.Gravatar Pierre-Marie Pédrot2018-04-30
| * Wrap VM bytecode used on the OCaml side in an OCaml block.Gravatar Pierre-Marie Pédrot2018-04-30
|/
* Merge PR #6958: [lib] Move global options to their proper place.Gravatar Maxime Dénès2018-04-30
|\
* \ Merge PR #6892: Cleanup implementation of normalize_context_set a bitGravatar Pierre-Marie Pédrot2018-04-28
|\ \
* | | Always print explanation for univ inconsistency, rm Flags.univ_printGravatar Gaëtan Gilbert2018-04-26
* | | Merge PR #6908: Move VM global tables from C to MLGravatar Maxime Dénès2018-04-20
|\ \ \
| | * | universe normalisation: put equivalence class partition in UGraphGravatar Gaëtan Gilbert2018-04-13
| |/ / |/| |
* | | Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Gravatar Maxime Dénès2018-04-12
|\ \ \
* \ \ \ Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationGravatar Pierre-Marie Pédrot2018-04-09
|\ \ \ \
| * | | | Fix #6956: Uncaught exception in bytecode compilationGravatar Maxime Dénès2018-04-06
| | | | * [lib] Move global options to their proper place.Gravatar Emilio Jesus Gallego Arias2018-04-02
| | |_|/ | |/| |
| | * | [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
| |/ /
* / / Expliciting and taking advantage of a representation invariant in Esubst.Gravatar Pierre-Marie Pédrot2018-03-27
|/ /
| * More efficient reallocation of VM global tables.Gravatar Pierre-Marie Pédrot2018-03-26
| * Moving the VM global atom table to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
| * Moving the VM global data to a ML reference.Gravatar Pierre-Marie Pédrot2018-03-26
|/
* Fix expected number of arguments for cumulative constructors.Gravatar Gaëtan Gilbert2018-03-09
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6769: Split closure cache and remove whd_bothGravatar Maxime Dénès2018-03-09
|\ \
| | * Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| | * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| |/ |/|
* | Merge PR #6747: Relax conversion of constructors according to the pCuIC modelGravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Maxime Dénès2018-03-09
|\ \ \
| * | | Fix SR breakage due to allowing fixpoints on non-rec valuesGravatar Matthieu Sozeau2018-03-08
| | * | Relax conversion of constructors according to the pCuIC modelGravatar Matthieu Sozeau2018-03-08
| |/ / |/| |
* | | Add empty description for @raise statements to satisfy ocamldocGravatar mrmr19932018-03-05
* | | Replace invalid tag @raises in ocamldoc comments with @raiseGravatar mrmr19932018-03-05