| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
|
|
|
|
Hugo Herbelin proposed to modify directly the function
"check_correct_par" to simplify commit c12b430
(see the pullrequest's discussion).
Note that the constructor "LocalNonPar" has now three arguments (instead
of two). In LocalNonPar (n,i,l) n denotes the position among real
arguments (ie. ignoring letins), i is the rel index of the expecting argument
in the context of parameters and l is the index of the inductive.
|
|
|
|
This is necessary for the patch for #4221 (817308ab5) to work.
|
|
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
|
|
|
hash-consing, so as to avoid having too many kinds of equalities with
same name.
|
|
constant/inductive/constructor kernel_name pairs rather than viewing
them from only the user or canonical part.
Hopefully more uniformity in Constr.hasheq (using systematically == on
subterms).
A semantic change: Cooking now indexing again on full pairs of kernel
names rather than only on the canonical names, so as to preserve user
name.
Also, in pair of kernel names, ensuring the compact representation is
used as soon as both names are the same.
|
|
The hash function exported by the interface ought to respect the equality.
Therefore, we only use the syntactic hash for the hashconsing module while
using the canonical hash in the API.
|
|
compatible with a unique bound module name counter which is not
synchronous with the backtracking).
We changed hash-consing of kernel name pairs to a purely memory
management issue, not trying to exploit logical properties such as
"syntactically equal user names have syntactically same canonical
names" (which is true in a given logical session, but not in memory,
at least because of residual values after backtracking).
|
|
|
|
|
|
|
|
|
|
I was not seeing the warning due to the 10 deprecation warnings before
it...
|
