aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-11Move the side-effect role out of Entries into Evd.Pierre-Marie Pédrot
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-07Merge PR #10308: Merge the two sources of monomorphic constraints for side-ef...Gaëtan Gilbert
2019-06-06Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.Vincent Laporte
2019-06-06Merge the two sources of monomorphic constraints for side-effects.Pierre-Marie Pédrot
2019-06-04Remove the discharge segment from vo files.Pierre-Marie Pédrot
2019-06-04Slightly tweak the representation of dischargeable opaque proofs.Pierre-Marie Pédrot
2019-06-04Do not substitute opaque constants when discharging.Pierre-Marie Pédrot
2019-05-31Fix #10268: vio2vo produces incorrect term when discharging.Pierre-Marie Pédrot
2019-05-29Merge PR #10252: Various dynamic assertions and cleanups in opaque typingMaxime Dénès
2019-05-29Merge PR #10248: Move the Discharge module in the kernel and merge it with Co...Maxime Dénès
2019-05-28Merge PR #10258: Remove the delayed universe table from object files.Enrico Tassi
2019-05-28Merge PR #10133: mind_kelim is the highest allowed sort instead of a listPierre-Marie Pédrot
2019-05-27Remove the delayed universe table from object files.Pierre-Marie Pédrot
2019-05-27Merge PR #10249: More precise type for export and inlining of private constantsMaxime Dénès
2019-05-27Fix #10251: Type-checking of polymorphic opaque constr entry types is broken.Pierre-Marie Pédrot
2019-05-27Specific code path for opaque polymorphic constants.Pierre-Marie Pédrot
2019-05-27Ensure dynamically that non-opaque definitions are always side-effect free.Pierre-Marie Pédrot
2019-05-27Ensure dynamically that opaque definitions come with their type.Pierre-Marie Pédrot
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-26Code sharing inside Cooking.Pierre-Marie Pédrot
2019-05-26Actually merge Discharge into Cooking.Pierre-Marie Pédrot
2019-05-26Share API between Discharge and Cooking.Pierre-Marie Pédrot
2019-05-26Move the Discharge module into the kernel.Pierre-Marie Pédrot
2019-05-25Centralize the hashconsing of constant declarations.Pierre-Marie Pédrot
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-24Move body_of_constant_body to Global and specialize its uses.Pierre-Marie Pédrot
2019-05-24Statically ensure the content of delayed proofs in vio file.Pierre-Marie Pédrot
2019-05-24Remove a useless call to the Future API for opaque proofs in the STM.Pierre-Marie Pédrot
2019-05-24Remove a last use of opacity-piercing function in Safe_typing.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 2JPR
2019-05-21[build] Select uint63 using `ocamlc -config` variables.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:11:43 +0000