| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |/
|
|
|
| |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
inductive types)
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
The point is to emphasize stronglier when we are talking about
contexts or about arguments.
|
| | |/ /
|/| |
| | |
| | |
| | | |
The number of effective parameters was used where the number of
declarations in the signature of parameters should have been used.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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`
|
| |/ / / |
|
| | | |
| | |
| | |
| | |
| | | |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
evd: Move constrain_variables to an operation on UState
Necessary to check universe declarations correctly for deferred proofs
in particular.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| |/ |
|
| |\
| |
| |
| | |
top of the linking chain.
|
| |\ \
| | |
| | |
| | | |
from location in file
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Inductive-keyworded record failing even on non-dependent goal)
|
| | |_|_|/ /
|/| | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
A trick in counting spaces in a format was making the empty notation
not behaving correctly.
|
| | |_|/ /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | | |
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.
|
| |\ \ \ |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | | |
This removes a dependency from `G_vernac` to `Metasyntax`.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 53a50875 and a bit more: it also makes the check
for possibly ignoring formatting spaces irrelevant, since the previous
commit makes that curly brackets are not any more dropped for
printing.
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
| | |_|/
|/| |
| | |
| | | |
(from module List).
|
| | |/
|/| |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|_|/
|/| | |
| | | |
| | | | |
Use the functional interface understand_tcc instead.
|
| | |_|/
|/| |
| | |
| | | |
This was already the case, but the API was not exposing this.
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
y , z".
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We now only issue an error for locally specified (non)cumulativity
whenever it is the context (set locally or globally) is monorphic.
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \
| |_|_|/ /
|/| | | | |
|
| | | | | | |
|
| | | |/ /
| |/| | |
|
Maxime Dénès
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Hugo Herbelin
Gaëtan Gilbert
Matthieu Sozeau
Guillaume Melquiond
Paul Steckler
Amin Timany
Matej Košík