aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2020-03-19Remove spurious anomalies in kernel reductionGaëtan Gilbert
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
This module used to do retyping for the kernel in prototypes of SProp, but was switched to only relevance inference before the merge.
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-17Merge PR #11699: Comment difference between the 2 hashes on constrPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
Reviewed-by: SkySkimmer
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
Reviewed-by: SkySkimmer
2020-03-09Do not rely on the implicit declaration of caml_minor_collection.Guillaume Melquiond
This commit also prefixes young_ptr and young_limit along the way, so as to not rely on OCaml's compatibility layer. This is a gratuitous change, since this code is only meant to be compiled with OCaml < 4.10 anyway.
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
This could have been at the root of strange behaviours (read unsoundness).
2020-03-08Template polymorphism is now a property of the inductive block.Pierre-Marie Pédrot
For an inductive block to be template, all its components must also be. This is probably fixing a few soundness bugs in the process, but I do not want to think too much about it.
2020-03-08Do not hardcode specific handling of Prop levels in template poly.Pierre-Marie Pédrot
We also factorize a few checks by returning an option when looking for a potentially template universe.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:26:12 +0000