| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |\
| | |
| | |
| | | |
Was PR#339: Documenting type class options, typeclasses eauto
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
... in pose proof of large proof terms
|
| | | | | |
|
| |\| | | |
|
| | | |/
| |/| |
|
| | |\ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6.
This behavior of refine has changed three times in recent years, so
let's take the time to make up our mind and wait for a major release.
Btw, onhyps=None is not a sane way to express that a tactic should be
applied to all hypotheses.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We simply catch the RetypeError raised by the retyping function and translate
it into a user error, so that it is captured by the tactic monad instead of
reaching toplevel.
|
| |\| | |
|
| | |\ \
| | | |
| | | |
| | | | |
Was PR#263: Fast lookup in named contexts
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | | |
This does not affect the semantics of these functions.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This bug was introduced by 37ab45726, because the new apply_type function
was not checking that the new goal was indeed well-typed. We add this check
locally in the generalize dependent tactic.
|
| |\| | | |
|
| | |\ \ \
| | | |/
| | |/| |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
the case for clear and the conversion tactics.
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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".
|
| | | | | |
|
| | | | | |
|
| | | |/
| |/| |
|
| | | | |
|
| |\ \ \ |
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | |\ \ \
| | | |/
| | |/| |
|
| | | | |
| | | |
| | | |
| | | | |
(It was reducing also in hypotheses.)
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
calls are logged too. Using appropriate printer for reparsability of
the output.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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).
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
"Context.{Rel,Named}.fold_constr"
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.
If multiple modules define a function with a same name, e.g.:
Context.{Rel,Named}.get_type
those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This was showing up in some of Jason's examples, where an abstract had to
compute the weak head form of a huge term in order to find the corresponding
implicit arguments.
|
| | | |
| | |
| | |
| | | |
Suggested by @ppedrot
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| | |
| |
| |
| | |
Fixing by copying what Matthieu did for Clenvtac.clenv_refine.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | | |
|
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Théo Zimmermann
Hugo Herbelin
Matej Kosik
Matej Kosik
Emilio Jesus Gallego Arias
Pierre Letouzey