| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.
We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.
Of course, the question of what best unification error to give in the
presence of backtracking is still open.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | | |
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| | |/ / / / /
|/| | | | | |
|
| | | | |\ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ |
|
| |/ / / / / / / /
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
auto with * is an overkill for people who do not care to understand
what they really need. In these two cases, one lemma which was
available in the typeclass_instances hint db.
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We seized this opportunity to factorize the code for interning `pat
with more general pre-existing code.
More precisely: There was already a function to compute the free
variables of a pattern. Commit c6d9d4fb rewrote an approximation of it
and #5222 hits cases non-treated by this function. We remove the
partially-defined redundant code and use instead the existing code
since intern_cases_pattern, already called, was already doing this
computation. (In doing so, we discover a bug in merging names in the
presence of nested "as" clauses, which we fix in previous
commit. Additionally, intern_local_pattern was misleadingly overkill
to simply mean a folding on Id.Set.add and we avoid the detour.
|
| | | | | | | | | |
|
| | | | | |\ \ \ \
| | | | | |/ / /
| | | | |/| | | |
|
| |\ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Was introduced in 5268efdef, reverted then readded in 1be9c4d.
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
1969e10f25df0c913600099b7b98ea273a064017 introduced a check so a cast
in a pattern is not a fatal error.
We move this check to the internalization function, which is the
logical place to raise it, removing a bit boilerplate code.
|
| | |_|_|/ / / / / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
The type `raw_cases_pattern_expr` is used only in the interpretation
of notation patterns. Indeed, this should be a private type thus we
make it local to `Constrintern`; it makes no sense to expose it in the
public AST.
The patch is routine, except for the case used to interpret primitives
in patterns. We now return a `glob_constr` representing the raw
pattern, instead of the private raw pattern type. This could be
further refactored but have opted to be conservative here.
This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754
, see the commentaries there for more information about
`raw_cases_pattern_expr`.
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| |/ / / / / / / / |
|
| | | | | | | | | |
|
| | | | | | | | | |
|
| | |/ / / / / /
|/| | | | | | |
|
| |/ / / / / / |
|
| | | | | | | |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \
| | | | | | | |
| | | | | | | |
| | | | | | | | |
and 8.5/8.6 "refine"
|
| |\ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ |
|
| | | | | | | |/ / / |
|
| | | | | | | |\ \ \
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
"Print Assumptions".
|
| | | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
The rule is that any file misc/*.sh will now be automatically executed
from the test-file directory with appropriate environment variables
set. The test can use any auxiliary material which is put in a
directory of the same name as the test.
This avoids making the main Makefile more or more complex.
We loose some customization though (no more custom messages such as
printing of the number of universes in the test about the number of
necessary universes). We could preserve such customization if needed
but I did not consider it was worth the effort.
Warning: specific targets universes, deps-order, deps-checksum are
removed by consistency. Do instead "make misc/universes.log", etc., or
even "make misc" for all.
|
| | | | | | | | | | | |
|
| | | | | | | | | | | |
|
| | |_|_|_|/ / / / /
|/| | | | | | | | |
|
| | | | | | |\ \ \ \ |
|
| | | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
Hugo Herbelin
Maxime Dénès
Pierre-Marie Pédrot
Gaetan Gilbert
Théo Zimmermann
Pierre Courtieu
Emilio Jesus Gallego Arias
Jason Gross
Jason Gross