| Commit message (Collapse) | Author | Age |
... | |
| | | | | | | |
|
| |/ / / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
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.
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
wish #4129)
|
| |_|_|_|_|_|_|/
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
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.
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Since 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a universe binders were
declared twice for all records.
Since 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 this causes an
observable error for monomorphic records.
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We limit fixpoints to Finite inductive types, so that BiFinite
inductives (non-recursive records) are excluded from fixpoint
construction. This is a regression in the sense that e.g. fixpoints
on unit records were allowed before. Primitive records with
eta-conversion are included in the BiFinite types.
Fix deprecation
Fix error message, the inductive type needs to be recursive for fix to work
|
| | | | | | |/
| | | | | |/| |
|
|\ \ \ \ \ \ \
| |_|_|_|_|/ /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
Attempt to extract the current ongoing proof (request by
Clément Pit-Claudel on coqdev, and also #4129).
Evars are handled as axioms.
|
| |_|_|_|/ / / / / / / /
|/| | | | | | | | | | |
| | | | | | | | | | | |
| | | | | | | | | | | | |
Following up on #6791, we the option "Shrink Abstract".
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
a record.
|
| | | | | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| |_|_|_|_|_|/ / / / / / / /
|/| | | | | | | | | | | | | |
|
| | | | | | | | | | | | | | |
|
| | | | |/ / / / / / / / /
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
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.
|
| | |/ / / / / / / / / / |
|
| | | |/ / / / / / / /
| | |/| | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \
| |_|/ / / / / / / / /
|/| | | | | | | | | | |
|
|\ \ \ \ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | |
| | | | | | | | | | | | |
| | | | | | | | | | | | | |
size.
|
|\ \ \ \ \ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | |
| | | | | | | | | | | | | | |
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"
|
| | | | | | | | | | | | |
|
| | | | | | | | | | | | |
|
| | | |/ / / / / / / /
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
Fix new deprecation warnings in the standard library.
|
| | |/ / / / / / / / |
|
| |/ / / / / / / /
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
Noticed by Sigurd Schneider.
|
|/ / / / / / / /
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
We test the 3 possible scenarios. A more complete test would also
involved fake_ide.
c.f. #6793
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \
| |_|_|_|_|_|_|/ /
|/| | | | | | | |
| | | | | | | | | |
infinite eta-expansion)
|
| |_|/ / / / / /
|/| | | | | | | |
|
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
As per https://github.com/coq/coq/pull/6756/files#r168028764
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
| |_|/ / / / / / /
|/| | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
More precisely when matching
"f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z"
do not allow expansion of f since otherwise, we recursively have to
match "f t" with the same pattern.
|
| |_|_|_|_|/ / /
|/| | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Also changed the API of pr_subgoals now using labels.
Also removed a trailing space in printing existentials.
|
|\ \ \ \ \ \ \ \ |
|