| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\ \ \ \ \ \ \ \ \ |
|
| | |_|_|_|_|/ / / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | | |
(from module List).
|
| | |_|_|/ / / / /
|/| | | | | | | |
|
| | |_|_|/ / / /
|/| | | | | | |
|
| | | | | | | | |
|
| | |_|/ / / /
|/| | | | |
| | | | | |
| | | | | | |
from Detyping.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This one is a continuation of e2a8edaf59 which was βι-normalizing the
hypotheses created by a "match". We forgot to do it for "let" and
"if". This is what this commit is doing.
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Formerly, mk_refgoals in logic.ml was applying full βι on new Meta-based goals.
We simulate part of this βι-normalization in pose_all_metas_as_evars.
I suspect that we don't βι-normalize goals more than in 8.4 by doing
that, since all Metas would have eventually gone to mk_refgoals, but
difficult to know for sure as there were probably metas turned to
evars (and hence a priori not βι-normalized) even when logic.ml was
used more pervasively.
However, βι-normalizing is a priori a better heuristic than no
βι-normalizing, independently of what it was in 8.4 and before (even
if, ideally, I would personally lean towards preferring a
"chirurgical" substitution with reduction only at the place of
substitution).
|
| | | | | | |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Use the functional interface understand_tcc instead.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |/ / / / /
|/| | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This surprising bug was caused by an Id.Set which was ordering
solutions to variable-projection problems in ascii order.
We fix it by re-considering the variables involved in the solutions
using the declaration order.
Note that in practice, this implies preferring a dependent solution
over a non-dependent one.
|
| | | |_|_|/
| |/| | | |
|
| | | | | | |
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is important for externalization big terms. We were indeed allocating
twice as much as needed lists for the application node case, as the
Array.map_to_list function is exactly List.map o Array.to_list.
We could probably tweak this function instead, at the expense that order of
evaluation is not guaranteed. I'm not willing to do that though.
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This essentially means storing the abstract universe context in the typeclass
data, and abstracting it when necessary.
|
| | | | |
| | | |
| | | |
| | | | |
We return the abstract context instead of an arbitrary instantiation.
|
| | | | | |
|
| |\ \ \ \ |
|
| | |/ / /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
|
| |\ \ \ \
| |/ / /
|/| | |
| | | | |
constant".
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Delaying also some computation needed for printing to the time of
really printing it.
|
| |\ \ \ \ |
|
| | |/ / /
|/| | | |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | | |
Also giving the proper local flag to the hint registration, even on a
Global instance, since the instance discharge manage itself the
redefinition of a hint.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Ltac pattern-matching was requiring dependent variables to be named.
This "natural" expectation is however not guaranteed by unification:
an evar can be dependent on an anonymous variable, resulting in
elaborated terms with dependent anonymous variables (see example in
file 5434.v).
This commit "fixes" the problem by not requiring that dependent
variables are named in ltac pattern-matching. Ltac pattern-matching
names itself these anonymous dependent variables, using the same
strategy as the printer (i.e. using "H" to display such
internally-anonymous dependent variables).
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
Incorrect environment was used when checking subtyping information of
inductive types.
|
| | | | |
|
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Paul Steckler
Guillaume Melquiond
Julien Forest
Matej Košík
Pierre-Marie Pédrot
Théo Zimmermann
Amin Timany