| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
#3125)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This function returns InProp or InSet for inductive types only when
the inductive type has been explicitly truncated to Prop or
(impredicative) Set.
For instance, singleton inductive types and small (predicative)
inductive types are not truncated and hence in Type.
|
| | |
| |
| |
| | |
recursive functions.
|
| |\ \ |
|
| | |/
|/|
| |
| |
| | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| | |
| |
| |
| | |
Also nicer error when the constraints are impossible.
|
| |/
|
|
| |
Before sometimes there were lists and strings.
|
| |\
| |
| |
| | |
constructs.
|
| | |
| |
| |
| |
| |
| | |
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
| | |
| |
| |
| | |
Note the problem with `create_evar_defs`.
|
| | |
| |
| |
| |
| |
| |
| | |
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
| |/
|
|
|
|
| |
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
| |\
| |
| |
| | |
unbound rel
|
| | |
| |
| |
| |
| |
| |
| | |
When an evar is undefined we need to substitute inside the evar instance.
With help from @herbelin and @psteckler to identify the issue from a
large test case.
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | | |
The message is the "Conversion test raised an anomaly" one.
|
| | | |/
| | |
| | |
| | | |
We do up to `Term` which is the main bulk of the changes.
|
| | |/
|/|
| |
| | |
This will allow to merge back `Names` with `API.Names`
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We refine the criterion for selecting a projection. Before PR#924 it
was alphabetic (i.e. morally "random" up to alpha-conversion). After
PR#924 it was chronological.
We refine a bit more by giving priority to simple projections when
they exist over projections which include an evar instantiation (and
which may actually be ill-typed).
|
| |/ /
| |
| |
| | |
This is a first step towards some of the solutions proposed in #6008.
|
| |\ \
| | |
| | |
| | | |
variables).
|
| |\ \ \
| | | |
| | | |
| | | | |
alphabet
|
| | |/ /
|/| |
| | |
| | | |
This fixes also #5731, #6035, #5364.
|
| | | |
| | |
| | |
| | |
| | | |
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
?INTERNAL#42 style is ugly
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | | |
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).
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
let-ins and non-recursively uniform parameters
|
| |\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
4e70791).
|
| | |_|_|/ / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
Maxime Dénès
Hugo Herbelin
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Matthieu Sozeau
Pierre-Marie Pédrot
Matthieu Sozeau