| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
|
