aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2020-04-01Merge PR #11306: Centralize the flag handling native compilation.Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-03-31Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit ↵Hugo Herbelin
arguments Ack-by: SkySkimmer Ack-by: gares Reviewed-by: herbelin
2020-03-31Merge PR #11889: Fix a spelling mistake in the code: s/magicaly/magically/Enrico Tassi
2020-03-31Include review suggestionsGaëtan Gilbert
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-30[typeclasses] Use label for `fail_evar` parameter.Emilio Jesus Gallego Arias
This makes code a bit more clear.
2020-03-30Merge PR #11921: Remove some cruft from Reductionops API.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: herbelin Ack-by: ppedrot
2020-03-28Remove a useless reversed variant in Vars.Pierre-Marie Pédrot
2020-03-28Remove some cruft from Reductionops API.Pierre-Marie Pédrot
- Removal of exported types and functions that were unused. - Moving ad-hoc functions that were used once in the codebase to their call site.
2020-03-24Merge PR #11858: Rename Retypeops -> RelevanceopsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-23s/magicaly/magically/Jason Gross
2020-03-23Merge PR #11867: Fix the computation of recursive principles with let-bindings.Enrico Tassi
Reviewed-by: gares
2020-03-20Fix the computation of recursive principles with let-bindings.Pierre-Marie Pédrot
We use a more robust implementation that does not assume that the type of the inductive is in ζ-normal form. This code path is not exercised, because due to the kernel typing algorithm, let-bindings in the type of a recursor are expanded away.
2020-03-19[declare/lemmas] Make inference hook exception-freeEmilio Jesus Gallego Arias
This is a step towards cleanup of the `start` lemma path.
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-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
The current implementation was seemingly never thought for this kind of semantics. Everything is superglobal by construction, notably hint database creation and naming schemes. The new mode feels a bit hackish to me, at some point this should be fully reimplemented from scratch with a clear design in mind.
2020-03-13[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
2020-03-11Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constantsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-09Fix #9930: "change" replaces 0-param projections by constantsGaëtan Gilbert
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-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-25Fix backtraces in conversion anomalies caught by Reductionops.Pierre-Marie Pédrot
The call to is_anomaly actually destroyed the backtrace, because it would call arbitrary code, in particular in Himsg which relied internally on raising exceptions.
2020-02-24Merge PR #11623: Deprecate unsafe_type_ofPierre-Marie Pédrot
Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-20Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-18Deprecate unsafe_type_ofGaëtan Gilbert
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: mattam82
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 #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
The standard use is to repeat the option keywords in lowercase, which is basically useless. En passant add doc entry for Dump Arith.
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-11Reinforcing the role of type "typing_constraint".Hugo Herbelin
WithoutTypeConstraint says it can be a term. In particular, if it has manual implicit arguments, these will be allowed only in leading lambdas. I.e. it can start with "fun {x}" but not with "forall {x}". New constructor UnknownIfTermOrType allows to be both a term or a type. In particular, if it allowed start both with "fun {x}" and "forall {x}".
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: maximedenes
2020-02-11Merge PR #11554: Fix #11553: magicaly_constant_of_fixbody checks existence ↵Pierre-Marie Pédrot
of made up constant Reviewed-by: ppedrot
2020-02-09Fix #11553: magicaly_constant_of_fixbody checks existence of made up constantGaëtan Gilbert
2020-02-07various unsafe_type_of -> type_of_variable in funindGaëtan Gilbert
This is the easy part of removing unsafe_type_of, as type_of_variable doesn't return (or even take as argument) an evar map.
2020-02-06unsafe_type_of -> type_of in Pretyping.pretype_refGaëtan Gilbert
We already thread the evar map
2020-02-06unsafe_type_of -> type_of in Unification.applyHeadGaëtan Gilbert
We already thread the evar map
2020-02-06unsafe_type_of -> type_of in Tacred.pattern_occsGaëtan Gilbert
This function already returns the evar map so no problem.
2020-02-06unsafe_type_of -> get_type_of in casesGaëtan Gilbert
It goes in an error message so should be fine.
2020-02-04Remove `unsafe_type_of` from `Coercion`Maxime Dénès
We thread explicitly the evar map everywhere for this purpose.
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-02-03Do not return a full term in Evarsolve alias expansion.Pierre-Marie Pédrot
The only user is merely observing whether this can be an rel / var alias.
2020-02-03Delay lifting in Evarsolve aliasing.Pierre-Marie Pédrot
It turns out that eagerly computing the lift of huge terms when it is not used is not great for performance. Fixes part of #11488.
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-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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 05:00:02 +0000