aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2020-03-08[exn] [nit] Remove not very useful re-raises.Emilio Jesus Gallego Arias
Cleanup: IMHO most of the re-raises here are not worth it.
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
The current behaviour could be considered as sub-optimal, but it probably doesn't matter in practice as this happens when serializing side-effects.
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
We make the primitives for backtrace-enriched exceptions canonical in the `Exninfo` module, deprecating all other aliases. At some point dependencies between `CErrors` and `Exninfo` were a bit complex, after recent clean-ups the roles seem much clearer so we can have a single place for `iraise` and `capture`.
2020-02-26[native compiler] Allow to set OCaml include dirs for compilationEmilio Jesus Gallego Arias
`Nativelib` currently assumes that objects are built in some particular directories, but this is not true in some cases, for example, when building with Dune. We add a new option `-nI` to allow clients to specify the OCaml include dirs.
2020-02-26[native compiler] Allow to set the output directory for cmx objectsEmilio Jesus Gallego Arias
This is useful in order to implement native support in Dune for example, which as of today as strict target rules. Hopefully this option could go away; it is really internal, but I've chosen to document it.
2020-02-24Do not perform a universe diff when typing opaque constants.Pierre-Marie Pédrot
Apart from being an ugly hack in the kernel, the universe-adding function is already robust to redundant universes anyways.
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
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-02-13Merge PR #11424: Check instance length in type_of_{inductive,constructor}Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-12Merge PR #11544: Cleanup some globref related manipulationsPierre-Marie Pédrot
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-02-12Merge PR #11569: Remove unused Environ.push_constraints_to_envPierre-Marie Pédrot
Reviewed-by: ppedrot
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
Instead of various termops and globnames aliases.
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
The previous system was from before globref was in the kernel.
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
Reviewed-by: ppedrot
2020-02-08Fixing wrong comments in context.ml.Hugo Herbelin
2020-02-07Merge PR #11528: Checker does not rely on Monomorphic fieldsGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-06Merge PR #11478: Nicer kernel universe error for inductivesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-05Store the template polymorphic context inside the TemplateArity node.Pierre-Marie Pédrot
This was the only part in the kernel that really relied on the contents of the Monomorphic node.
2020-02-04Merge PR #11491: Small side effect cleanupPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-02-03Merge PR #11481: Do not rely on Libobject for the current environment in ↵Maxime Dénès
extraction. Reviewed-by: maximedenes
2020-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
It was virtually unused except in ssr, and there is no reason to clutter the kernel with irrelevant code. Fixes #9390: What is the purpose of the function "kind_of_type"?
2020-01-30export_private_constants doesn't use the [constr in_univ_ctx] argumentGaëtan Gilbert
2020-01-30Fix 11483Pierre Roux
Performance bug of PrimFLoat.compare with native_compute When adapting Coq.Interval with @erikmd and @silene, we noticed that PrimFLoat.compare is taking a lot of time with native_compute (much more than with vm_compute). This comes from the implementation using the OCaml polymorphic comparison instead of the float comparison.
2020-01-30Do not rely on Libobject for the current environment in extraction.Pierre-Marie Pédrot
Instead, we export in Safe_typing the current module declaration.
2020-01-29Nicer kernel universe error for inductivesGaëtan Gilbert
Not sure if it's possible to see it without a plugin.
2020-01-27Small API additions to kernel/univGaëtan Gilbert
- allow viewing the internal representation of uglobal and universe (with universe, this replaces the "map" function. I kept exists and for_all as they felt somewhat convenient) - add universe set and map modules (currently unused but they're natural)
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
preparation for direct discharge
2020-01-14infercumulativity: take less argumentsGaëtan Gilbert
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
We make a temporary directory for these files and cleanup at process exit. The temporary directory means we don't have to guess what extensions ocaml will produce, we can just delete everything there. We use Lazy to avoid spamming unused directories when ahead-of-time compiling without actually using native casts / nativenorm (typically stdlib files). Sadly ocaml has "create temp file" but not "create temp dir", so we have to copy the name generation code. Fix #10495
2020-01-07cleanup: do not use recargs when computing the reloc table for ctorsGaëtan Gilbert
This doesn't actually have anything to do with positivity AFAICT, we just want the number of non-parameter arguments.
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. ↵Guillaume Melquiond
(Fixes #11321) It has the added advantage of performing 6 less 64-bit operations per long multiplication.
2019-12-22Simplify equality of 63-bit integers.Guillaume Melquiond
The sign bit is supposed to be zero, so no need to mask it out. If it was not zero, most of the algorithms in this file would fail horribly.
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 ↵Pierre-Marie Pédrot
~strict flag Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
Reviewed-by: ppedrot
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
Issue #10603
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 19:41:41 +0000