| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |_|/ / /
|/| | | |
| | | | |
| | | | | |
We also make the code of [compact] in kernel/univ.ml a bit clearer.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | | |
Since this is an open bug, it is of lesser importance but
non-deterministic tests are a real problem OTOH.
|
| |\ \ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | | |
We use a lower level function that accesses the proof without raising an
anomaly. This is a direct candidate for backport, so I used a V82 API but
eventually this API should be cleaned up.
|
| |/ / /
| | |
| | |
| | |
| | | |
This is done by not failing for fix/cofix while translating from
glob_constr to constr_pattern.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
Answering to commit about #5500: we don't know in general if the
return predicate T(y1,..,yn,x) in the intermediate step of a nested
pattern-matching is a sort, but we don't even know if it is
well-typed: retyping is not enough, we need full typing.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a quick fix to check in nested pattern-matching that the
return clause is typed by an arity (there was already a check when the
return clause was given explicitly - in the 3rd section of
prepare_predicate -; it was automatically typed by a sort when the
return clause was coming by pattern-matching with the type constraint,
since the type constraint is a type; but it was not done when the
predicate was derived from a former predicate in nested
pattern-matching).
Indeed, in nested pattern-matching, we know that the return predicate
has the form λy1..yn.λx:I(y1,..,yn).T(y1,..,yn,x) and we know that
T(v1,...,vn,u) : Type for the effective u:I(v1,..,vn) we are matching
on, but we don't know if T(y1,..,yn,x) is itself a sort (e.g. it can
be a "match" which reduces to a sort when instantiated with v1..vn,
but whose evaluation remains blocked when the y1..yn are variables).
Note that in the bug report, the incorrect typing is produced by small
inversion. In practice, we can raise the anomaly also without small
inversion, so we fix it in the general case. See file 5500.v for
details.
|
| |/ |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative
inductive would try to generate a constraint [i = j] and use
cumulativity only if this resulted in an inconsistency. This is
confusingly different from the behaviour with [Type] and means
cumulativity can only be used to lift between universes related by
strict inequalities. (This isn't a kernel restriction so there might
be some workaround to send the kernel the right constraints, but
not in a nice way.)
See modified test for more details of what is now possible.
Technical notes:
When universe constraints were inferred by comparing the shape of
terms without reduction, cumulativity was not used and so too-strict
equality constraints were generated. Then in order to use cumulativity
we had to make this comparison fail to fall back to full conversion.
When unifiying 2 instances of a cumulative inductive type, if there
are any Irrelevant universes we try to unify them if they are
flexible.
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.
This fixes #6313.
Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.
|
| |/
|
|
|
|
|
| |
Following up on #6791, we remove support refolding in reduction.
We also update a test case that was not properly understood, see the
discussion in #6895.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | | |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| |_|_|_|/ /
|/| | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
When there is more than one variable to declare we stop trying to
attach global universes (ie monomorphic or section polymorphic) to one
of them.
|
| | | |/ / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Following up on #6791, we remove:
- `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes`
- `Match Strict` a deprecated NOOP.
|
| | |/ / / |
|
| | |/ / |
|
| |\ \ \
| |/ /
|/| | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This test was actually checking that evar-containing terms were making the
VM fail. Obviously this is not the case anymore, so the test is now invalid.
|
| | | |/
| | |
| | |
| | | |
Following up on #6791, we remove the option "Standard Proposition Elimination"
|
| | | | |
|
| | |/ |
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
the concl
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Computation of the sort of the inductive type was done before ensuring
that the arguments of the inductive type had the correct types,
possibly brutally failing with `NotArity` in case one of the types
expected to be typed with an arity was not so.
|
| | |/ /
|/| | |
|
| | | | |
|
| | |/
|/|
| |
| |
| | |
by doing the same thing as `zify_nat` does for `nat.pred`.
This fixes #6602.
|
| |\ \
| |/
|/| |
|
| | | |
|
| |\ \
| |/
|/| |
|
| |\ \ |
|
| | | | |
|
| | |/
|/|
| |
| | |
Fixes BZ#5726.
|
| |\ \ |
|
| |\ \ \ |
|
| | | | | |
|
Maxime Dénès
Théo Zimmermann
Pierre-Marie Pédrot
Jasper Hugunin
Gaëtan Gilbert
Hugo Herbelin
Emilio Jesus Gallego Arias
Enrico Tassi
Anton Trunov
Matthieu Sozeau
Joachim Breitner
Tej Chajed
Cyprien Mangin