| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Getting closer from before when the bug was introduced + test.
|
|
|
|
|
|
|
|
This removes a dependency on wit_tactic in Constrintern.
|
|
|
|
|
|
We also move the Ltac-specific grammar to its folder.
|
|
|
|
|
|
|
|
Previously, newlines were missing if a node had no children.
|
|
This removes a space (making the final letter of the right-aligned columns line come right before the vertical separators, rather than overlapping them), and left-aligns "tactic", as it was in Tobias' original code, which I think is easier to read. (This way, the alignment of the headers matches the alignment of the entries.)
|
|
|
|
The previous commit did not apply the beta reduction for compatibility on the
correct goal. We rather apply it on the first generated subgoal. This fixes the
ergo contrib.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Changes:
- data structures are purely functional (so retracting do work)
- profiling data flows towards master using the feedback bus
- master aggregates the data on printing
|
|
|
|
calls are logged too. Using appropriate printer for reparsability of
the output.
|
|
|
|
The problem came from the fact that the legacy beta-reduction occurring
after a rewrite was wrongly applied to the side-conditions of the
rewriting step. We restrict it to the correct goal in this patch.
|
|
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).
|
|
|
|
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 an overlook. There was no reason to let it in the tactics/ folder,
as is was semantically part of the Ltac implementation.
|
|
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.
|
|
|
|
|
|
when the rewrite lemma doesn't typecheck or does not
correspond to a relation.
|
|
|
|
|
|
|
|
|
|
It should use evar instantiations eagerly during unification of
the lhs of the lemma, as in 8.4.
|
|
|
|
match.""
We apply this patch to trunk so that it is integrated in 8.6.
This reverts commit 0eb08b70f0c576e58912c1fc3ef74f387ad465be.
|
