aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2019-05-21Merge PR #10174: Further cleanup of the side-effect machineryGaëtan Gilbert
2019-05-21Merge PR #10144: Fix #9919: conversion functions are non-linearHugo Herbelin
2019-05-20Do not perform the section variable check on global recipes.Pierre-Marie Pédrot
2019-05-20Ensure statically that declarations built by Term_typing are direct.Pierre-Marie Pédrot
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-05-19Make the type of constant bodies parametric on opaque proofs.Pierre-Marie Pédrot
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-15Merge PR #10151: Clean up the API for side-effectsGaëtan Gilbert
2019-05-15Merge PR #9905: [vm] x86_64 registersMaxime Dénès
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-05-14Reduce the attack surface of Opaqueproof.Pierre-Marie Pédrot
2019-05-11Generalize map_named_val to handle whole declarations.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-09Merge PR #10046: [primitive integers] Make div21 implems consistent with its ...Maxime Dénès
2019-05-03Remove now useless commented codePierre Roux
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
2019-05-02Add union in Map interfaceMaxime Dénès
2019-04-30Merge PR #9952: Remove `constr_of_global_in_context`Pierre-Marie Pédrot
2019-04-30[vm] Backport from OCamlPierre Roux
2019-04-30[vm] PPC64 registersPierre Roux
2019-04-30[vm] ARM registersPierre Roux
2019-04-30[vm] Arm 64 registersPierre Roux
2019-04-30[vm] x86_64 registersPierre Roux
2019-04-29Merge PR #9925: [vm] Protect accu and coq_envMaxime Dénès
2019-04-23Merge PR #9962: [native compiler] Encoding of constructors based on tagsPierre-Marie Pédrot
2019-04-16[doc] [kernel] Add docstrings for native interface functions.Emilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
2019-04-15[vm] Protect accu and coq_envPierre Roux
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
2019-04-12Remove `constr_of_global_in_context`Maxime Dénès
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
2019-03-31Merge PR #9800: Less conv_tab allocations when pushing relevances, esp skip_p...Pierre-Marie Pédrot
2019-03-28[dune] Don't have `lib` depend on `dynlink`Emilio Jesus Gallego Arias
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...Maxime Dénès
2019-03-20Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on applic...Gaëtan Gilbert
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
2019-03-18Less conv_tab allocations when pushing relevances, esp skip_patternGaëtan Gilbert
2019-03-18Remove Term_typing.translate_mind indirectionGaëtan Gilbert
2019-03-18Merge PR #9740: Make NotConvertibleVect exception internal to typeopsPierre-Marie Pédrot
2019-03-14Put [@inline] on CClosure.Mark functionsGaëtan Gilbert
2019-03-14Switch order eqappr/check relevance in conversion.Gaëtan Gilbert
2019-03-14mutable relevance marks in fconstrGaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:29:00 +0000