| Age | Commit message (Collapse) | Author |
|---|
|
Printing metas still happens relatively often. From the user point of
view, no need to know that it is different from an evar, so the
notation ?M42 as it was before is much lighter. As for developers
looking for debugging information, they will easily suspect that it is
internally a meta because of the "M".
This reverts "Proposing meta names more distinguishable from evar
names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead).
|
|
|
|
The bug was caused by an inconsistency in different part of the code
for deciding where cutting the context in between recursively uniform
parameters and non-recursively uniform ones when let-ins were in the
middle. We fix it by using uniformly "context_chop".
|
|
context obtained by ltac pattern-matching)
|
|
Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability.
Tough maybe it signals too much an unelegant debugging flavor?
|
|
The main fix is to use is_ident_soft. The rest of the commit is to
provide something a bit more appealing than "?M-1".
|
|
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
|
|
|
|
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
|
|
|
|
|
anonymous variables)
|
|
|
|
The code from Universes what essentially a duplicate of the one from EConstr,
but they were copied for historical reasons. Now, this is not useful anymore,
so that we remove the implementation from Universes and rely on the one from
EConstr.
|
|
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
|
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
|
|
|
|
|
|
|
implementation from Detyping.
|
|
|
|
|
|
(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.
|
|
|
|
|
