aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2018-04-06Fix #6956: Uncaught exception in bytecode compilationMaxime 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-27Expliciting and taking advantage of a representation invariant in Esubst.Pierre-Marie Pédrot
2018-03-26More efficient reallocation of VM global tables.Pierre-Marie Pédrot
2018-03-26Moving the VM global atom table to a ML reference.Pierre-Marie Pédrot
2018-03-26Moving the VM global data to a ML reference.Pierre-Marie Pédrot
2018-03-09Fix expected number of arguments for cumulative constructors.Gaëtan Gilbert
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Merge PR #6769: Split closure cache and remove whd_bothMaxime Dénès
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Merge PR #6747: Relax conversion of constructors according to the pCuIC modelMaxime Dénès
2018-03-09Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesMaxime Dénès
2018-03-08Fix SR breakage due to allowing fixpoints on non-rec valuesMatthieu Sozeau
2018-03-08Relax conversion of constructors according to the pCuIC modelMatthieu Sozeau
2018-03-05Add empty description for @raise statements to satisfy ocamldocmrmr1993
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortMaxime Dénès
2018-03-04Remove whd_both from the kernel.Pierre-Marie Pédrot
2018-03-04Pass the constant cache as a separate argument in kernel reduction.Pierre-Marie Pédrot
2018-03-03Handling 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-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-24Merge PR #6784: New IR in VM: ClambdaMaxime Dénès
2018-02-23New IR in VM: Clambda.Maxime Dénès
2018-02-23Fix map iterator on nativelambda.Maxime Dénès
2018-02-21Merge PR #6740: Adding a sanity check on inductive variance subtyping.Maxime Dénès
2018-02-19Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Maxime Dénès
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2018-02-15Adding a sanity check on inductive variance subtyping.Pierre-Marie Pédrot
2018-02-14Factorize the relocations in the on-disk VM representation.Pierre-Marie Pédrot
2018-02-14Use a more compact representation for bytecode relocations stored on disk.Pierre-Marie Pédrot
2018-02-14Do not use global variables for VM bytecode compilation in Cemitcodes.Pierre-Marie Pédrot
2018-02-14Remove the unsafe bytes conversion function in Cemitcodes.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 17:14:51 +0000