| Commit message (Collapse) | Author | Age |
... | |
|
|
|
| |
This is a first step towards some of the solutions proposed in #6008.
|
|
|
| |
fix spelling mistake. reword message to be in the Present Perfect tense instead of the 3rd person present because action is completed with respect to the theorem not some unknown third person.
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
| | |
|
|/
|
|
|
| |
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
|
|
|
|
| |
Compared to the original proposition (01f848d in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
|\ |
|
|\ \ |
|
| | | |
|
| | | |
|
| |/
|/|
| |
| |
| | |
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).
|
|\ \ |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | | |
It was introduced in 8.5 for compatibility with a 8.4 bug.
|
|/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
As was questioned on Stack Overflow and discussed on Gitter, reduction
of the conclusion of the goal was done up to n+1 times for a failing
call to "constructor" on an inductive type of n constructors. We do it
at most once.
Reworking the layout of the code at the same time.
|
| |/
|/|
| |
| | |
The bug was introduced in 1559f73.
|
|\ \ |
|
| |/
|/|
| |
| |
| | |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
Inductive-keyworded record failing even on non-dependent goal)
|
| |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This changes the implementation of "constructor" from
constructor 1 + ... + constructor n + fail
to
constructor 1 + ... + constructor n.
|
| |_|/
|/| | |
|
| |/
|/|
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| | |
The fix covers the case of a non-dependent goal with unavailable
dependent case analysis: destruct was not seeing that it could still
use non-dependent case analysis.
|
| |
| |
| |
| |
| | |
The code generating the projection was unconditionally generating
pattern-matchings, although this is incorrect for primitive records.
|
|\ \ |
|
|\ \ \
| |_|/
|/| | |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
In functions match_eqdec and check_unused_names
|
| | | | | | |
|
| |_|_|/ /
|/| | | |
| | | | |
| | | | | |
Only in ml files that are not related to Coq commands
|
|\ \ \ \ \ |
|
| |_|_|/ /
|/| | | | |
|
| | | | | |
|
| |_|/ /
|/| | | |
|
| |/ /
| | |
| | |
| | |
| | | |
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
|
|\ \ \
| |/ /
|/| | |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`,
`Miscprint`) to their proper place as they were declared in different
`mllib` files than the one in their directory.
In some cases this could be refined but we don't do anything fancy, we
just reflect the status quo.
|
| |_|_|/ /
|/| | | | |
|