| Commit message (Collapse) | Author | Age |
... | |
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
This is more precise and probably clearer (see e.g. thread
"Understanding auto" on coq-club).
|
|\| | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
In `Ftactic` the number of results could desynchronise with the number
of goals when some goals were solved by side effect in a different
branch of a `DISPATCH`.
See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
|
|\| | | |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We simply catch the RetypeError raised by the retyping function and translate
it into a user error, so that it is captured by the tactic monad instead of
reaching toplevel.
|
|\| | | |
|
| | | | |
|
| |\ \ \
| | | | |
| | | | |
| | | | | |
Was PR#263: Fast lookup in named contexts
|
| | | | |
| | | | |
| | | | |
| | | | | |
between proofs in tactic injection, with a side-effect on inversion.
|
|\| | | | |
|
| |\ \ \ \
| | | |/ /
| | |/| | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
This does not affect the semantics of these functions.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This bug was introduced by 37ab45726, because the new apply_type function
was not checking that the new goal was indeed well-typed. We add this check
locally in the generalize dependent tactic.
|
| |\| | | |
|
| | |\ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#293: Fix #4762 (eauto weaker than auto).
|
| | | | | | |
|
| | |/ / / |
|
|\| | | | |
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
the case for clear and the conversion tactics.
|
|\| | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.
|
|/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.
The previously common idom:
if pi2 kind (* polymorphic *) then ... else ...
becomes:
if kind.polymorphic then ... else ...
To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".
|
| | | | |
| | | | |
| | | | |
| | | | | |
One of them revealed a true bug.
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
~True.
Found 1 incompatibility in tested contribs and 3 times the same
pattern of incompatibility in the standard library. In all cases, it
is an improvement in the form of the script.
New behavior deactivated when version is <= 8.5.
|
| | | | | |
|
| | | | | |
|
| | |/ /
| |/| | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
|\ \ \ \ |
|
|\ \ \ \ \
| | |/ / /
| |/| | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is not needed, as the terms are then checked up to unification or
convertibility.
|
|\| | | | |
|
| |\ \ \ \
| | | |/ /
| | |/| | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
(It was reducing also in hypotheses.)
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
calls are logged too. Using appropriate printer for reparsability of
the output.
|
| | | | | |
|