| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
Remove predicative flag and adapt to new invariant where every universe
must be declared, ensuring it is >= Set, safe_repr is not necessary
anymore.
|
|
declare new universes (e.g. with).
|
|
|
|
|
|
assumed.
|
|
|
|
The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
|
|
Was left over after Hugo's 9c732a5c878b.
|
|
Substitution on bound modules was incorrectly extended without sequential
composition.
|
|
Now distinguishes between bound modules (Top#X) and submodules (Top.X).
Could be useful for the regular printer as well (e.g. in error messages), but I
don't know what the compatibility constraints are, so leaving it as it is for
now.
|
|
|
|
When reifying a 31-bit integer after a VM computation, we check that no bit
outside the 31 LSB is set to 1.
|
|
|
|
Previously, the kernel would silently fall back to standard conversion.
|
|
On 64 bits architectures, integers could have some of their 32 msb set to 1
internally in the VM. When read back to a Coq term, this was not observable. But
an equality test would fail. From the user point of view, the symptom was that
vm_compute; reflexivity would succeed but the subsequent Qed would fail.
Bug reported by Tahina Ramananandro.
|
|
ADDMULDIVINT31 was missing pops in some cases
|
|
|
