aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2018-06-17Merge PR #7635: Define rec_declaration in terms of prec_declaration.Maxime Dénès
2018-06-17Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Maxime Dénès
2018-06-13Merge PR #7677: [api] Remove MisctypesPierre-Marie Pédrot
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-12[VM] Rename reloc -> cenvMaxime Dénès
2018-06-10[VM] Remove projection names from structured constants.Maxime Dénès
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
2018-06-05Define rec_declaration in terms of prec_declaration.SimonBoulier
2018-06-05More straightforward native compilation of primitive projections.Pierre-Marie Pédrot
2018-06-05Use projection indices in native compilation rather than constant names.Pierre-Marie Pédrot
2018-06-05Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8Pierre-Marie Pédrot
2018-06-05Merge PR #7646: Fix #4714: Stack overflow with native computePierre-Marie Pédrot
2018-06-05Merge PR #7495: Fix restrict_universe_contextMatthieu Sozeau
2018-06-04Fix #7631: native_compute fails to compile an example in Coq 8.8Maxime Dénès
2018-06-04Merge PR #7418: Actually take advantage of the normalization status of kernel...Maxime Dénès
2018-06-04Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Maxime Dénès
2018-06-01Merge PR #7234: Reduce circular dependency constants <-> projectionsMaxime Dénès
2018-05-31Fix #4714: Stack overflow with native computeMaxime Dénès
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated aliases from `Names`.Emilio Jesus Gallego Arias
2018-05-30[api] Reintroduce `Names.global_reference` aliasEmilio Jesus Gallego Arias
2018-05-30Fix restrict_universe_contextGaëtan Gilbert
2018-05-28Fix #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-05-28Make some comments more precise about compilation of cofixpointsMaxime Dénès
2018-05-28Less confusing debug printing of setfield bytecode instructionMaxime Dénès
2018-05-25Merge pull request #7569 from ppedrot/clean-newringAssia Mahboubi
2018-05-23Renaming miscellaneous internal smart functions.Hugo Herbelin
2018-05-23Moving Rtree.smart_map into Rtree.Smart.map.Hugo Herbelin
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-21Simplify the newring hack.Pierre-Marie Pédrot
2018-05-16Merge PR #7079: Remove naked pointers from the VMMaxime Dénès
2018-05-13Fix #4403: insufficient handling of type-in-type in kernel.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-05-01Actually take advantage of the normalization status of kernel closures.Pierre-Marie Pédrot
2018-04-30Adapt the VM GC hook to handle the no-naked-pointers option flag.Pierre-Marie Pédrot
2018-04-30Make the VM accumulator look like an OCaml block.Pierre-Marie Pédrot
2018-04-30Wrap VM bytecode used on the OCaml side in an OCaml block.Pierre-Marie Pédrot
2018-04-30Merge PR #6958: [lib] Move global options to their proper place.Maxime Dénès
2018-04-28Merge PR #6892: Cleanup implementation of normalize_context_set a bitPierre-Marie Pédrot
2018-04-26Always print explanation for univ inconsistency, rm Flags.univ_printGaëtan Gilbert
2018-04-20Merge PR #6908: Move VM global tables from C to MLMaxime Dénès
2018-04-13universe normalisation: put equivalence class partition in UGraphGaëtan Gilbert
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-04-09Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:57:21 +0000