aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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-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
2020-03-06Also check for monomorphic universes in side-effects certificates.Pierre-Marie Pédrot
2020-03-06Abstract away the API for side-effect certificates.Pierre-Marie Pédrot
2020-03-06Make explicit that the side-effect certificate trust is all-or-nothing.Pierre-Marie Pédrot
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-26[native compiler] Allow to set OCaml include dirs for compilationEmilio Jesus Gallego Arias
2020-02-26[native compiler] Allow to set the output directory for cmx objectsEmilio Jesus Gallego Arias
2020-02-24Do not perform a universe diff when typing opaque constants.Pierre-Marie Pédrot
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-13Merge PR #11417: Move kind_of_type from the kernel to EConstr.Enrico Tassi
2020-02-13Merge PR #11424: Check instance length in type_of_{inductive,constructor}Pierre-Marie Pédrot
2020-02-12Merge PR #11544: Cleanup some globref related manipulationsPierre-Marie Pédrot
2020-02-12Merge PR #11569: Remove unused Environ.push_constraints_to_envPierre-Marie Pédrot
2020-02-12Check instance length in type_of_{inductive,constructor}Gaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
2020-02-11Remove unused Environ.push_constraints_to_envGaëtan Gilbert
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-02-09Merge PR #11550: Fixing wrong comments in context.mlPierre-Marie Pédrot
2020-02-08Fixing wrong comments in context.ml.Hugo Herbelin
2020-02-07Merge PR #11528: Checker does not rely on Monomorphic fieldsGaëtan Gilbert
2020-02-06Merge PR #11478: Nicer kernel universe error for inductivesPierre-Marie Pédrot
2020-02-05Store the template polymorphic context inside the TemplateArity node.Pierre-Marie Pédrot
2020-02-04Merge PR #11491: Small side effect cleanupPierre-Marie Pédrot
2020-02-03Merge PR #11481: Do not rely on Libobject for the current environment in extr...Maxime Dénès
2020-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:10:58 +0000