| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.
While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
|
| | |
| | |
| | |
| | | |
And some code simplification.
|
| |/
|/|
| |
| | |
And a bit of code simplification.
|
|/
|
|
|
| |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
|
|
|
|
|
|
|
|
|
|
| |
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
| |
|
| |
|
|
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
|
|
|
| |
This will allow to merge back `Names` with `API.Names`
|
|
|
|
| |
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.
|
|
|
|
|
| |
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.
|
|\ |
|
|\ \
| | |
| | |
| | | |
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.
|
| |
| |
| |
| |
| |
| | |
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.
|
|\ \ |
|
|\ \ \
| |_|/
|/| | |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | | |
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.
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is probably the hardest case of them all, because tclABSTRACT fundamentally
relies on the names of universes from the constant instance being the same as
the one in the current goal. Adding to that the fact that the kernel is doing
strange things when provided with a polymorphic definition with body universe
constraints, it turns out to be a hellish nightmare to handle properly.
At some point we need to clarifiy this in the kernel as well, although we
leave it for some other patch.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
As per @JasonGross's request who described a use case for this option in
https://coq.inria.fr/bugs/show_bug.cgi?id=5633 and pending an alternative
solution for this use case.
|
|/ / |
|
| | |
|
| |
| |
| |
| |
| | |
Also fixing a bug of get_next_hyp_position when the hypothesis is the
oldest of the context (see test in ltac.v).
|
|/
|
|
|
| |
It allows in particular to have "Info" on tactic "assert" and
derivatives not to give an "<unknown>".
|
|\ |
|
|\ \ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/
|/| |
|