aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
...
| | | | * [native_compute] Delay computations with toplevel matchGravatar Maxime Dénès2018-06-11
* | | | | [VM] Remove projection names from structured constants.Gravatar Maxime Dénès2018-06-10
| |_|_|/ |/| | |
| * | | Fix #7615: Functor inlining drops universe substitution.Gravatar Pierre-Marie Pédrot2018-06-07
|/ / /
| * | Define rec_declaration in terms of prec_declaration.Gravatar SimonBoulier2018-06-05
* | | More straightforward native compilation of primitive projections.Gravatar Pierre-Marie Pédrot2018-06-05
* | | Use projection indices in native compilation rather than constant names.Gravatar Pierre-Marie Pédrot2018-06-05
|/ /
* | Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Pierre-Marie Pédrot2018-06-05
|\ \
* \ \ Merge PR #7646: Fix #4714: Stack overflow with native computeGravatar Pierre-Marie Pédrot2018-06-05
|\ \ \
* \ \ \ Merge PR #7495: Fix restrict_universe_contextGravatar Matthieu Sozeau2018-06-05
|\ \ \ \
| | | * | Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Maxime Dénès2018-06-04
| |_|/ / |/| | |
* | | | Merge PR #7418: Actually take advantage of the normalization status of kernel...Gravatar Maxime Dénès2018-06-04
|\ \ \ \
* \ \ \ \ 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
|\ \ \ \ \ \
| | | | | * | Fix #4714: Stack overflow with native computeGravatar Maxime Dénès2018-05-31
| * | | | | | 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 restrict_universe_contextGravatar Gaëtan Gilbert2018-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
| | | * Simplify the code that handles trust of side-effects in kernel typing.Gravatar Pierre-Marie Pédrot2018-05-27
| |_|/ |/| |
* | | 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
| | * Actually take advantage of the normalization status of kernel closures.Gravatar Pierre-Marie Pédrot2018-05-01
| |/ |/|
| * 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
| |/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 08:14:27 +0000