| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
| |
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>".
|
|\ |
|
|\ \ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/
|/| |
|
|/
|
|
|
|
|
|
|
| |
As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.
We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Now when a partial with-binding is given the unsolved parameters are
left quantified.
A letin is added when mixing (fun x => ...) and with-bindings.
|