aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2020-04-06Clean and fix definitions of options.Théo Zimmermann
- Provide new helper functions in `Goptions` on the model of `declare_bool_option_and_ref`; - Use these helper functions in many parts of the code base (encapsulates the corresponding references); - Move almost all options from `declare_string_option` to `declare_stringopt_option` (only "Warnings" continue to use the former). This means that these options now support `Unset` to get back to the default setting. Note that there is a naming misalignment since `declare_int_option` is similar to `declare_stringopt_option` and supports `Unset`. When "Warning" is eventually migrated to support `Unset` as well, we can remove `declare_string_option` and rename `declare_stringopt_option` to `declare_string_option`. - For some vernac options and flags that have an equivalent command-line option or flag, implement it like the standard `-set` and `-unset`.
2020-04-03Be cleverer and do not hopelessly rezip a term when not needed.Pierre-Marie Pédrot
A quick analysis showed that most of the calls to whd do not lead to a term which further triggers reduction, so there is no point in refolding a potentiall huge term for no reason.
2020-03-31Merge PR #11684: Remove spurious anomalies in kernel reductionPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-30Merge PR #11951: Remove a useless reversed variant in Vars.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: erikmd
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 ↵Maxime Dénès
than our own. Ack-by: aaronpuchert Ack-by: gadmm Reviewed-by: maximedenes Ack-by: ppedrot Reviewed-by: proux01
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
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 15:07:07 +0000