| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
|
|
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.
|
|
This is a step towards cleanup of the `start` lemma path.
|
|
This module used to do retyping for the kernel in prototypes of SProp,
but was switched to only relevance inference before the merge.
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
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.
|
|
Reviewed-by: ppedrot
|
|
|
|
This could have been at the root of strange behaviours (read unsoundness).
|
|
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`.
|
|
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.
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Instead of various termops and globnames aliases.
|
|
The previous system was from before globref was in the kernel.
|
|
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}".
|
|
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes
|
|
of made up constant
Reviewed-by: ppedrot
|
|
|
|
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.
|
|
We already thread the evar map
|
|
We already thread the evar map
|
|
This function already returns the evar map so no problem.
|
|
It goes in an error message so should be fine.
|
|
We thread explicitly the evar map everywhere for this purpose.
|
|
|
|
The only user is merely observing whether this can be an rel / var alias.
|
|
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.
|
|
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"?
|
|
- 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)
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: maximedenes
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
The command `Set NativeCompute Timing` causes calls to `native_compute`
(as well as kernel calls to the native compiler) to emit separate timing
information about compilation, execution, and reification. This allows
more fine-grained timing of the native compiler without needing to set
the `-debug` flag.
|
|
|
|
We typecheck arguments like previously, using bidirectionality hints,
but ultimately replace them with user-provided arguments on which we
replay coercion traces.
This is a fix which should be easy to backport, but there are two
directions of future work:
- Coercion traces for `Program` coercions (in these cases, we currently
use the inferred arguments)
- Separate the Coercion API in two phases: inference and application of
coercions. It will make the approach taken here cleaner, and probably
make it easier to interleave typing steps with coercion inference.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
clauses in pattern matching decompilation algorithm
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
The `Print Canonical Projections` command now can take constants and prints only
the unification rules that involves or are synthesized from given constants.
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
|
|
|
