aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2020-01-30export_private_constants doesn't use the [constr in_univ_ctx] argumentGaëtan Gilbert
2020-01-30Fix 11483Pierre Roux
2020-01-30Do not rely on Libobject for the current environment in extraction.Pierre-Marie Pédrot
2020-01-29Nicer kernel universe error for inductivesGaëtan Gilbert
2020-01-27Small API additions to kernel/univGaëtan Gilbert
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-21Typo in a comment of univ.mli.Hugo Herbelin
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
2020-01-14infercumulativity: take less argumentsGaëtan Gilbert
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
2020-01-07cleanup: do not use recargs when computing the reloc table for ctorsGaëtan Gilbert
2020-01-07minor cleanup template_polymorphic_univs: check_levels returns boolGaëtan Gilbert
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2019-12-27Add critical-bugs entry, tests-suite file, and code comment.Guillaume Melquiond
2019-12-22Use a more straightforward algorithm for mulc on 32-bit architectures. (Fixes...Guillaume Melquiond
2019-12-22Simplify equality of 63-bit integers.Guillaume Melquiond
2019-12-22Do not hide constants from the compiler.Guillaume Melquiond
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...Pierre-Marie Pédrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
2019-12-17failwith -> caml_failwithGuillaume Munch-Maccagnoni
2019-12-17Fatal error in VM if SIGINT was seen but no exception occured.Guillaume Munch-Maccagnoni
2019-12-17Fix signal polling for OCaml 4.10Guillaume Munch-Maccagnoni
2019-12-17[VM] fix volatile declarationGuillaume Munch-Maccagnoni
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-12[vm] Untabify the VM C code.Emilio Jesus Gallego Arias
2019-12-07Section.t is never emptyGaëtan Gilbert
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
2019-11-26indTyping: error instead of anomaly for ill-formed templateGaëtan Gilbert
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-22Use the relevance flag in CClosure rel contexts in an efficient way.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:59:50 +0000