| Commit message (Collapse) | Author | Age |
... | |
| | |
|
|\| |
|
| | |
|
| | |
|
|\| |
|
| | |
|
|\| |
|
| |\
| | |
| | |
| | | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.
|
|\| | |
|
| |\ \
| | | |
| | | |
| | | | |
Was PR#319: More error tagging, try to fix bug 5135
|
| |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#334: Fix bug 5031 : should not be an anomaly
|
| | | | |
| | | | |
| | | | |
| | | | | |
not an anomaly
|
|\| | | | |
|
| |/ / / |
|
| | |/
| |/|
| | |
| | |
| | | |
reconsider_conv_pbs -> reconsider_unif_constraints
consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The word "increment" is more appropriate in this case than "lifting".
The world "lifting", in computer science, usually denotes something else:
https://en.wikipedia.org/wiki/Lambda_lifting
|
| | | |
|
| |/
| |
| |
| |
| |
| |
| |
| | |
The current tag system in `Pp` is generic, which implies we must choose
a tagging function when calling a printer.
For console printing there is a single choice, thus this commits adds it
a few missing cases.
|
|\| |
|
| | |
|
|\| |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
This fixes the stack overflow part of the bug, even if the tactic is still quite
slow. The offending functions have been written in a tail-recursive way.
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
|\ \
| | |
| | |
| | | |
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
|
| | |
| | |
| | |
| | |
| | |
| | | |
There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
|
| |
| |
| |
| | |
One of them revealed a true bug.
|
|\ \
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We untangle many dependencies on Ltac datastructures and modules from the
lower strata, resulting in a self-contained ltac/ folder. While not a plugin
yet, the change is now very easy to perform. The main API changes have been
documented in the dev/doc/changes file.
The patches are quite rough, and it may be the case that some parts of the
code can migrate back from ltac/ to a core folder. This should be decided on
a case-by-case basis, according to a more long-term consideration of what is
exactly Ltac-dependent and whatnot.
|
| | | |
|
| | | |
|
|\ \ \
| |/ /
|/| /
| |/ |
|
| |
| |
| |
| | |
esprit d'escalier : is now also fixed for R
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
|
|\ \ \
| | |/
| |/| |
|
| |\ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
(This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)
|
| | | | |
|
|\| | | |
|
| |\| | |
|
| | | | |
|