| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |
|
| | |\ |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#350: tclDISPATCH: more informative error message
|
| | |\ \ \
| | | |/
| | |/| |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
| | |\| | |
|
| |/ / / |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| | |
"expected _n_ tactics" -> "exected _n_ tactics, was given _k_".
Also affect other similar tacticals from `Proofview`.
I used that for debugging once, I thought I might as well propose it for
mergeing.
|
| | |\
| | |
| | |
| | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | | | |
|
| | |\ \
| | |/
| |/|
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | | |
We return an option type, as constraints were always dropped if the boolean
was false. They did not make much sense anyway.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Before this patch, this module was a member of the library folder, which had
little to do with its actual use. A tiny part relative to global registering
of universe names has been effectively moved to the Global module.
|
| | | | |
|
| |\| | |
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#321: Handling of section variables in hints
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| |\| | | |
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Refine fix for bug #4763, fixing #5149
Tactic [Refine.solve_constraints] and global option
Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.
Fix test-suite files too.
|
| | | | |
|
| | | | |
|
| | |/
| |
| |
| |
| |
| |
| |
| | |
due to cleared/reverted section variables.
This fixes the get_type_of but requires keeping information
around about the section hyps available in goals during resolution.
It's optimized for the non-section case (should incur no cost there),
and the case where no section variables are cleared.
|
| | |
| |
| |
| |
| |
| | |
This function does the same thing as "Names.Id.List.mem" so:
- I deleted the "Namegen.to_avoid" function and
- replaced all calls of "Namegen.to_avoid" to calls of "Names.Id.List.mem"
|
| | |
| |
| |
| |
| |
| |
| | |
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
|
| |\| |
|
| | |
| |
| |
| |
| | |
When printing evar constraints, we ensure that every variable from the
rel context has a name.
|
| |\| |
|
| | | |
|
| | | |
|
| |\| |
|
| | |\
| | |
| | |
| | | |
Was PR#263: Fast lookup in named contexts
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
goal is under focus and which support returning a relevant output.
|
| | |/ |
|
| |\ \ |
|
| |\ \ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | | |
Essentially, we do not reconstruct the named_context_val when the rel_context
is empty.
|
| | | |
| | |
| | |
| | |
| | | |
Before computing the whd_evar-form of the arguments of an evar, we first
check that it is indeed defined.
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
composition operator.
Short story:
This pull-request:
(1) removes the definition of the "right-to-left" function composition operator
(2) adds the definition of the "left-to-right" function composition operator
(3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead.
Long story:
In mathematics, function composition is traditionally denoted with ∘ operator.
Ocaml standard library does not provide analogous operator under any name.
Batteries Included provides provides two alternatives:
_ % _
and
_ %> _
The first operator one corresponds to the classical ∘ operator routinely used in mathematics.
I.e.:
(f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x
We can call it "right-to-left" composition because:
- the function we write as first (f4) will be called as last
- and the function write as last (f1) will be called as first.
The meaning of the second operator is this:
(f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x
We can call it "left-to-right" composition because:
- the function we write as first (f1) will be called first
- and the function we write as last (f4) will be called last
That is, the functions are written in the same order in which we write and read them.
I think that it makes sense to prefer the "left-to-right" variant because
it enables us to write functions in the same order in which they will be actually called
and it thus better fits our culture
(we read/write from left to right).
|
| | | | |
|
| | | | |
|
Enrico Tassi
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Matthieu Sozeau
Arnaud Spiwack
Matej Kosik
Matthieu Sozeau
Matej Kosik