| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
| |
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).
Fixing similar error in pretyping.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- Introduced an error: fold was counting in the wrong direction and I
did not test it. Sorry.
- Substitution from params-with-let to params-without-let was still
not correct.
Hopefully everything ok now. Eventually, we should use canonical
combinators for that: extended_rel_context to built the instance and
and a combinator apparently yet to define for building a substitution
contracting the let-ins.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
projections.
- lift accounting for the record missing in computing the subst from
fields to projections of the record
- substitution for parameters should not lift the local definitions
- typo in building the latter (subst -> letsubst)
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
For instance,
Inductive a (x:=1) := C : a -> True.
was wrongly reporting
Error: The type of constructor C
is not valid; its conclusion must be
"a" applied to its parameter.
Also "simplifying" explain_ind_err.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Universes are now represented in the VM by a structured constant containing the
global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
constructor arguments, which has to be prevented.
Was showing up for instance when evaluating [cons _ list (nil _)] with
a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.
Patch written with Benjamin Grégoire.
|
| |
|
|
|
| |
Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
|
| | |
|
| |
|
|
|
|
|
|
| |
polymorphic definitions.
- This implementation passes universes in separate arguments and does not
eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
|
| | |
|
| |
|
|
|
|
| |
When F is a Functor, doing an 'Include F' triggers the 'Include Self'
mechanism: the current context is used as an pseudo-argument to F.
This may fail with a subtype error if the current context isn't adequate.
|
| |
|
|
| |
Was introduced in b06d3badb (15 Jul 2015).
|
| | |
|
| |
|
|
|
|
|
| |
to compensate decompose_lam_n_assum which does not count let-ins.
Any idea on a uniform and clear naming scheme for this kind of
decomposition functions?
|
| |
|
|
|
|
|
|
| |
Was introduced by seemingly unrelated commit
fd62149f9bf40b3f309ebbfd7497ef7c185436d5.
The currently policy is to avoid exposing global references in the kernel
interface when easily doable.
|
| |
|
|
|
|
|
|
|
| |
Using the same hack as in the kernel: VM conversion is a reference to
a function, updated when modules using C code are actually linked.
This hack should one day go away, but always linking C code may produce some
other trouble (with the OCaml debugger for instance), so better be safe
for now.
|
| | |
|
| | |
|
| |
|
|
| |
Previously, the kernel was silently switching back to the standard conversion.
|
| | |
|
| |
|
|
|
| |
This commit has no impact, since l2r is always false in practice due to
the definition of default_conv.
|
| | |
|
| |
|
|
|
| |
Stdlib does not compile when l2r flag is actually taken into account. We should
investigate...
|
| | |
|
| |
|
|
|
| |
Used to replace the standard conversion by the VM. Not so useful, and
implemented using a bunch of references inside and outside the kernel.
|
| |
|
|
| |
Became unused after c47b205206d832430fa80a3386be80149e281d33.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
direct aliases are ok, and indices should not be made polymorphic. Fixes NFix.
|
| | |
|
| |
|
|
| |
This commit is a follow-up to a51cce369b9c634a93120092d4c7685a242d55b1
|
| |
|
|
|
| |
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
| |
|
|
| |
Add a flag to disallow minimization to set
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Given the way Lib.extract_hyps is coded if the const_hyps field
of a constant declaration contains a named_context that does not
have the same order of the one in Environment.env, discharging is
broken (as in some section variables are not discharged).
If const_hyps is computed by the kernel, then the order is correct by
construction. If such list is provided by the user, the order is not
granted.
We now systematically sort the list of user provided section hyps.
The code of Proof using is building the named_context in the right
order, but the API was not enforcing/checking it. Now it does.
|
| | |
|
| |
|
|
|
|
|
| |
context
Let-bound definitions can be opaque but the whole universe context
was not gathered to be discharged at section closing time.
|
| |
|
|
|
|
| |
According to their polymorphic/non-polymorphic status, which
imply that universe variables introduced with it are assumed
to be >= or > Set respectively in the following definitions.
|
| | |
|
| |
|
|
|
| |
For polymorphic and non-polymorphic parameters and definitions, fixes
bugs #4298, #4294
|
| | |
|
Matthieu Sozeau
Guillaume Melquiond
Hugo Herbelin
Enrico Tassi
Maxime Dénès
Gregory Malecha
Pierre Letouzey
Matthieu Sozeau