aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2020-06-19Merge PR #12531: Fast inductive compilationGaëtan Gilbert
2020-06-19Do not reallocate named_context_val of the pretyping environment.Pierre-Marie Pédrot
2020-06-17Use an efficient data structure for VM compilation indexing.Pierre-Marie Pédrot
2020-05-25Merge PR #12344: Cleanup noisy prefixesPierre-Marie Pédrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Cleanup: remove noisy "sec_" prefixes in section.mlGaëtan Gilbert
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-22Remove # keywords in PrimitivePierre Roux
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
2020-04-14Merge PR #12084: [warnings] Be silent about the `set_tag` warning.Pierre-Marie Pédrot
2020-04-13Fix #11783 Require in SectionGaëtan Gilbert
2020-04-13Partial import inductive(..)Gaëtan Gilbert
2020-04-12[warnings] Be silent about the `set_tag` warning.Emilio Jesus Gallego Arias
2020-04-10[sideeff] Don't use polymorphic equality to check for empty side-effectsEmilio Jesus Gallego Arias
2020-04-10Merge PR #12039: Do not erase native files in debug modePierre-Marie Pédrot
2020-04-07Do not erase native files in debug modeMaxime Dénès
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-04-03Be cleverer and do not hopelessly rezip a term when not needed.Pierre-Marie Pédrot
2020-03-31Merge PR #11684: Remove spurious anomalies in kernel reductionPierre-Marie Pédrot
2020-03-30Merge PR #11951: Remove a useless reversed variant in Vars.Gaëtan Gilbert
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
2020-03-28Remove a useless reversed variant in Vars.Pierre-Marie Pédrot
2020-03-27Merge PR #11102: Use the Alloc_small macro from the OCaml runtime rather than...Maxime Dénès
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
2020-03-19Remove spurious anomalies in kernel reductionGaëtan Gilbert
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-17Merge PR #11699: Comment difference between the 2 hashes on constrPierre-Marie Pédrot
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
2020-03-12Remove a positivity check when Check Positivity is offSimonBoulier
2020-03-11Comment difference between the 2 hashes on constrGaëtan Gilbert
2020-03-10Merge PR #11764: Simplify mutual template polymorphismGaëtan Gilbert
2020-03-09Do not rely on the implicit declaration of caml_minor_collection.Guillaume Melquiond
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
2020-03-08Template polymorphism is now a property of the inductive block.Pierre-Marie Pédrot
2020-03-08Do not hardcode specific handling of Prop levels in template poly.Pierre-Marie Pédrot
2020-03-08[exn] [nit] Remove not very useful re-raises.Emilio Jesus Gallego Arias
2020-03-06Actually take advantage of the universes contained in side-effect certificates.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:51:44 +0000